top | item 21824267

(no title)

jcora | 6 years ago

Can lisps place arbitrary code in types and formally verify complex properties of stateful systems--all in the same language? Doubt it. Lisp isn't the epitome of power.

discuss

order

shakna|6 years ago

... Yes. Of course they can.

Lisp is usually an academic language, which means research into type systems and type safety frequently takes place in it.

ACL2 is a theorum prover written in Common Lisp [0]. And not just a random project either, but something AMD, ARM, IBM, etc. have used.

[0] https://en.wikipedia.org/wiki/ACL2

jcora|6 years ago

This is not a practical language with dependent types tho lol

throwawaybbb|6 years ago

Yes. That's the point, you will write the dsl to do that in scheme. Then use that to solve the original problem. Abstractions on top of abstractions.

jcora|6 years ago

No. You can write a compiler for any language in Scheme, but it's disingenuous to say that Scheme has that language's features. There are many languages with way more powerful features than Scheme if you're comparing type systems.

iLemming|6 years ago

Checkout Little Typer and Clojure.Spec.

> Lisp isn't the epitome of power.

Lisp is the epitome of simplicity. If the foundations based on simplicity you can do very powerful things.

braythwayt|6 years ago

Lisp in general is not the epitome of simplicity. Lisp-2s like Common Lisp add some cognitive load for those used to simpler languages (although Lisp-2s have their advantages).

And of course, Lisps that include meta-object protocols (Flavours, Common Lisp again, &c.) deliver power, very elegantly, but for people unfamiliar with them, there is a learning curve to climb.