undefined | Better HN

0 pointsjcora6y ago0 comments

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.

0 comments

shakna6y 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

jcoraOP6y ago

This is not a practical language with dependent types tho lol

throwawaybbb6y 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.

jcoraOP6y 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.

iLemming6y 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.

braythwayt6y 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.

iLemming6y ago

You're mistaking Lisp for a programming language. Which Lisp is not. Lisp is an idea (or rather a set of ideas), based on which different PLs can be implemented.

lispm6y ago

McCarthy not only had an idea, he and his team a specific programming language. It even had a manual.

This is the Lisp I manual:

http://bitsavers.org/pdf/mit/rle_lisp/LISP_I_Programmers_Man...

neonate6y ago

He said Lisps and Lisp-2s, so obviously knows this.

1 more reply

j / k navigate · click thread line to collapse

0 comments

shakna6y 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

jcoraOP6y ago

This is not a practical language with dependent types tho lol

throwawaybbb6y 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.

jcoraOP6y ago

iLemming6y 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.

braythwayt6y 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.

iLemming6y ago

You're mistaking Lisp for a programming language. Which Lisp is not. Lisp is an idea (or rather a set of ideas), based on which different PLs can be implemented.

lispm6y ago

McCarthy not only had an idea, he and his team a specific programming language. It even had a manual.

This is the Lisp I manual:

http://bitsavers.org/pdf/mit/rle_lisp/LISP_I_Programmers_Man...

neonate6y ago

He said Lisps and Lisp-2s, so obviously knows this.

1 more reply

j / k navigate · click thread line to collapse