5 ms·

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 o

by jcora 7y 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.

throwawaybbb 7y 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 7y 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.
shakna 7y 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 https://en.wikipedia.org/wiki/ACL2
- jcora 7y ago
  This is not a practical language with dependent types tho lol
iLemming 7y 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 7y 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.
  - iLemming 7y 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.
    - neonate 7y ago
      He said Lisps and Lisp-2s, so obviously knows this.
      - iLemming 7y ago
        I'm perfectly aware of that. My point stands - using a concrete language to generalize over some abstract ideas might be confusing for those who are unfamiliar. In general, Lisp dialects strive for simplicity. That is exactly the reason why Scheme was chosen for SICP.
        braythwayt 7y ago
        Can we agree on this? “Lisp dialects strive for elegance.” Elegance is not always synonymous with simplicity. For example, Smalltalk’s use of Class and Metaclass is very elegant, but most programmers encountering this for the first time would not call it “simple.” After they got over the hump and grok how the two things work together to serve as the foundation for Smalltalk’s OOP and allow programmers to alter Smalltalk’s OOP... Then the elegance emerges. I think elegance is a measure of the simplicity of a tool relative to the complexity of the problem domain, whereas simplicity feels like a more absolute measure.

by jcora 7y 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.

throwawaybbb 7y 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 7y 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.

shakna 7y 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 https://en.wikipedia.org/wiki/ACL2

jcora 7y ago
This is not a practical language with dependent types tho lol

iLemming 7y 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 7y 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.
- iLemming 7y 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.
  - neonate 7y ago
    He said Lisps and Lisp-2s, so obviously knows this.
    - iLemming 7y ago
      I'm perfectly aware of that. My point stands - using a concrete language to generalize over some abstract ideas might be confusing for those who are unfamiliar. In general, Lisp dialects strive for simplicity. That is exactly the reason why Scheme was chosen for SICP.
      - braythwayt 7y ago
        Can we agree on this? “Lisp dialects strive for elegance.” Elegance is not always synonymous with simplicity. For example, Smalltalk’s use of Class and Metaclass is very elegant, but most programmers encountering this for the first time would not call it “simple.” After they got over the hump and grok how the two things work together to serve as the foundation for Smalltalk’s OOP and allow programmers to alter Smalltalk’s OOP... Then the elegance emerges. I think elegance is a measure of the simplicity of a tool relative to the complexity of the problem domain, whereas simplicity feels like a more absolute measure.