6 ms·

> because it's perfectable. it's not perfect, but it is perfectable. you can write down properties about Lean, in Lean. Homoiconicity anyone? Lisp is one of t

by kleiba2 6mo ago

> because it's perfectable. it's not perfect, but it is perfectable. you can write down properties about Lean, in Lean. Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.

harperlee 6mo ago
The question then is how they plan to avoid The Lisp Curse (in my words, language giving you too much power makes you do weird things, and you attract people to like to use things a tad too powerful / generic, and you end up with an unproductive culture).
- codebje 6mo ago
  The primary culture around Lean is mathematicians looking to prove mathematics. AFAICT Lean is just about the right power for that. Agda, OTOH, is IMO the dependently typed language for type theorists, and does weird things, but "unproductive" is applicable only for a somewhat narrow view of productivity. I don't consider there to be a dependently typed language for writing programs that you just want to run, but I would be delighted to be corrected on that viewpoint!
  - harperlee 6mo ago
    I think Idris 2 is targeted more to programming than to doing math, no?
    - ux266478 6mo ago
      Yep. I also think it's the best designed out of any of them. As dependently typed languages have become more and more popular, I find it a bit sad that Idris has stayed relatively obscure.
      - addaon 6mo ago
        Since you've clearly looked at this a bit... would you give a sentence or two comparing Indris, F*, and the other lesser known players in this space (languages for both writing and formally verifying programs)? I find it a wide space to explore, and while ecosystem maturity seems like a huge deciding factor right now, I assume there's real and meaningful differences between the languages as well.
        ux266478 6mo ago
        Idris is rather unique in that the development flow involves writing out your program as a trellis with "holes", and you work through your codebase interactively filling those holes. It feels like Haskell with an even more powerful type system and a companion expert system to alleviate the burden that the type-system's power entails. You're still basically always in program-land, mentally. F* (and most other dependently-typed languages, or adjacent ones like Liquid Haskell) has a whole external SMT solver layer that lives outside of the language. Think like if SML modules were even less unified with the core language, and also most of your time was spent in that layer. They're really not fun to try and make complex software with, just because the context-switching required at scale is borderline inhuman. Lean has a unified proof-system in the language like Idris, but it has much the same grain as the languages with external SMT solvers. You're spending most of your mental time in proofsland, thinking primarily about how to prove what you want to do. That's because with how Lean as a language is set up, you're basically centering all your reasoning around the goal. If there's a problem, you're adjusting the structure of your reasoning, changing your proof strategy, or identifying missing lemmas, etc. You can kind of think of it as though Idris is "inside out" compared to most of the other dependently typed languages.
    - codebje 6mo ago
      It's been a little bit since I looked at Idris, so I'll take a closer look now. The QTT behind it struck me as interesting but I didn't play around with it much. Thanks for the tip!
  - yuppiemephisto 6mo ago
    lean IS that language https://github.com/alok/LeanPlot https://github.com/alok/LeanPlot
- hmokiguess 6mo ago
  Then again sometimes things don’t need to have productivity as a goal do they? Scale and context applies, could be seen as art even, an expression of someone’s psyche and their world model
- iLemming 6mo ago
  > you end up with an unproductive culture Practical Lispers would like to have a word - I've been witnessing extreme productivity on some teams. Modern Lisp dialects (Clojure and likes) largely broke library fragmentation and the "not invented here" tendency that were causing real tensions in Common Lisp. You realize that "The Lisp Curse" isn't some paper, survey or objective reflection? It's just someone's essay back from 2011 - an opinion. You can take it word-by-word and apply to say Javascript, and it would largely feel true - JS arguably has the worst fragmentation of any ecosystem; dozens of competing frameworks, build tools, bundlers, test runners; new frameworks constantly replacing old ones; "Javascript fatigue" is a real thing, etc., but nobody talks about "Curse of Javascript" I learned Lisp (once) and that opened up path to Clojure, Clojurescript, then Fennel, Janet and Clojure-Dart, libpython-clj, there's Jank that is about to break loose. And something opposite to fragmentation happened to me - all these incompatible runtimes became unified and controllable from the same substrate - I no longer feel like I'm having to switch between languages - the syntax and thinking stays stable. The runtime is just a deployment target. The curse essay says: "Lisp empowers fragmentation". Actual experience says: "Lisp provides unity across fragmentation that already existed"
  - pydry 6mo ago
    >You realize that "The Lisp Curse" isn't some paper, survey or objective reflection? It's just someone's essay back from 2011 - an opinion. It's also the deficit of code we actually use day to day that is actually written in lisp. I file it under the same heading as haskell - a language that clearly has useful ideas, but...
    - ux266478 6mo ago
      You're using Lisp software right now! I think this is the most treacherous assumption people tend to make about programming languages, for a few reasons. One of them is that we really don't have any way to measure software that we actually use day to day. Think about the software controlling your local water treatment plant, traffic lights, the software your local power company relies on, the software running the servers you connect to, and all the servers those things connect to. All the infrastructure in between and the infrastructure's own infrastructure. Allegro Lisp's customers are shotgun spread in industries like healthcare, finance and manufacturing. They're paying for it, so we can infer they're using it, but can anybody actually name what software is written in it? If we play six degrees of separation, accounting for the full gamut of every single computer that does something relevant to your life no matter how distant, how much of that software are you actually familiar with? The fact of the matter is that we genuinely have no broad picture. There is no introspective method to find out what software you are relying on in your day to day life, almost all of it is completely opaque and implicit. To ask "what software do I use?" is to ask an unanswerable question. So to then synthesize an answer is to work with an unsound, unsupported, incomplete conclusion, which is exactly how you end up assuming you don't use software written in Lisp, while directly using software written in Lisp (HN) Of course, even accounting for the epistemic issue, the premise is still flawed. ATS is a language with 'useful ideas, but...', Haskell is an aging pragmatic kitchen sink. Positioning the latter as the former is almost comedic.
- yuppiemephisto 6mo ago
  https://alok.github.io/assets/lean-position-paper.pdf https://alok.github.io/assets/lean-position-paper.pdf i talked about the lisp curse in this old paper. it's rough but explicitly mentions it
mghackerlady 6mo ago
I can't view the site (Org blocks github for reasons) but I suspect this would be a lot like forth if forth weren't so stack focused
- d-us-vb 6mo ago
  Forth is at this point more of a culture than a language. It's a culture about keeping designs simple so that they're understandable. Without this, Forth is only powerful for programmers who can keep a lot in their heads, but lots of Forth programs end up being write-once. Moore's view, as well as most other high-level Forthers preach simplicity above all; a code cleanliness that would make Uncle Bob blush. Lean and most type theoretic-based languages don't merely preach simplicity, they demand it. A function or type with a handful of terms or constructors might be provably inhabited/total, whereas one with 2 handfuls of terms or constructors might not be in a reasonable amount of time due to the exponential growth of the proof space. Factoring code optimally for provability yields the simplicity that Forth programmers are striving for.
  - blippage 6mo ago
    > Forth is at this point more of a culture than a language. As the saying goes, once you've seen one Forth, then you've seen one Forth. I've mucked around with my own Forths in the past, including one that recognises lexical type, so you could build something like a parser in Forth. I didn't take it that far. Forth is normally conceived as being built from the ground up, but if you're you're going to implement it in C or C++ then you can be more imaginative. I played around with colorforth for 5 minutes on a couple of occasions, but I ran away screaming. What - just what - the hell is going on? I'm sure it all works for Charles Moore, but for mere mortals it might as well be a klingon control panel. I think Moore effectively gave up on programming a couple of years ago? There was some strange modification in the guts of Windows and he couldn't get his environment to work any longer. He concluded that the game was not work the candle.
    - mghackerlady 6mo ago
      One of these days I want to make something forth-y as a shell language. I feel like it could work well there
iLemming 6mo ago
> Homoiconicity anyone? I'm just leaving this here for anyone interested, seems relevant: https://github.com/replikativ/ansatz https://github.com/replikativ/ansatz Ansatz is a verified programming library for Clojure built on the Calculus of Inductive Constructions (CIC) — the same type theory that powers Lean 4.
patrickmay 6mo ago
I came here to comment "We already have Lisp."
DonaldPShimoda 6mo ago
Hm. Homoiconicity is not a well-defined term (see, for example, Shriram Krishnamurthi's thoughts [0][1]), but even skimming over that fact, it is a syntactic property, while the quoted line is about semantics. Switching your language to Lisp (or one of its descendents) doesn't gain you anything semantically. [0] Shriram is an original member of the Racket project, so he's been working in the Lisp-like domain for at least 30 years and, specifically, he works in an offshoot of Lisp that is particularly concerned with questions of syntax. I think this establishes him as a reasonable citation for this topic. [1] https://parentheticallyspeaking.org/articles/bicameral-not-homoiconic/ https://parentheticallyspeaking.org/articles/bicameral-not-h...
- noLemming 6mo ago
  Well, okay Shriram said the term "homoiconicity" is fuzzy, but the underlying thing (the language of data and the language of programs being the same representation) is real and worth taking seriously. Citing him to wave away the whole concept is pretty wild misuse of the citation. They are refining the claim, not negating it. > doesn't gain anything semantically Syntactic properties create semantic affordances. The reason "code as data" matters isn't that the parentheses look a certain way - it's that the AST is a first-class citizen of the runtime data model. Those are semantic capabilities - they determine what programs can express and compute, especially at the meta level. The syntactic uniformity is the mechanism; the ability to write programs that construct and transform other programs, using the same tools as everything else, is the payoff. Homoiconicity doesn't make Lisp programs mean something different, but it gives you a more uniform and powerful meta-programming model.
  - DonaldPShimoda 6mo ago
    > Citing him to wave away the whole concept is pretty wild misuse of the citation. Good thing I didn't do that? > Syntactic properties create semantic affordances. I don't disagree with this. Benjamin Pierce defines type-checking in the opening pages of Types and Programming Languages as an operation over syntax, for example. My point was that the parent comment just kind of threw out "homiconicity" when somebody talked about writing properties about a language in that language, and those are entirely separate things. I was addressing a conflation of terms. The property that people generally refer to as "homoiconicity" is useful for things like writing macros, but it does not directly grant you access to any kind of property-checking capabilitiy. I mean, Rust's macro system is far from homoiconic (it's just an AST), but it gives you semantic capabilities. You know?

by kleiba2 6mo ago

harperlee 6mo ago

The question then is how they plan to avoid The Lisp Curse (in my words, language giving you too much power makes you do weird things, and you attract people to like to use things a tad too powerful / generic, and you end up with an unproductive culture).

codebje 6mo ago
The primary culture around Lean is mathematicians looking to prove mathematics. AFAICT Lean is just about the right power for that. Agda, OTOH, is IMO the dependently typed language for type theorists, and does weird things, but "unproductive" is applicable only for a somewhat narrow view of productivity. I don't consider there to be a dependently typed language for writing programs that you just want to run, but I would be delighted to be corrected on that viewpoint!
- harperlee 6mo ago
  I think Idris 2 is targeted more to programming than to doing math, no?
  - ux266478 6mo ago
    Yep. I also think it's the best designed out of any of them. As dependently typed languages have become more and more popular, I find it a bit sad that Idris has stayed relatively obscure.
    - addaon 6mo ago
      Since you've clearly looked at this a bit... would you give a sentence or two comparing Indris, F*, and the other lesser known players in this space (languages for both writing and formally verifying programs)? I find it a wide space to explore, and while ecosystem maturity seems like a huge deciding factor right now, I assume there's real and meaningful differences between the languages as well.
      - ux266478 6mo ago
        Idris is rather unique in that the development flow involves writing out your program as a trellis with "holes", and you work through your codebase interactively filling those holes. It feels like Haskell with an even more powerful type system and a companion expert system to alleviate the burden that the type-system's power entails. You're still basically always in program-land, mentally. F* (and most other dependently-typed languages, or adjacent ones like Liquid Haskell) has a whole external SMT solver layer that lives outside of the language. Think like if SML modules were even less unified with the core language, and also most of your time was spent in that layer. They're really not fun to try and make complex software with, just because the context-switching required at scale is borderline inhuman. Lean has a unified proof-system in the language like Idris, but it has much the same grain as the languages with external SMT solvers. You're spending most of your mental time in proofsland, thinking primarily about how to prove what you want to do. That's because with how Lean as a language is set up, you're basically centering all your reasoning around the goal. If there's a problem, you're adjusting the structure of your reasoning, changing your proof strategy, or identifying missing lemmas, etc. You can kind of think of it as though Idris is "inside out" compared to most of the other dependently typed languages.
  - codebje 6mo ago
    It's been a little bit since I looked at Idris, so I'll take a closer look now. The QTT behind it struck me as interesting but I didn't play around with it much. Thanks for the tip!
- yuppiemephisto 6mo ago
  lean IS that language https://github.com/alok/LeanPlot https://github.com/alok/LeanPlot
hmokiguess 6mo ago
Then again sometimes things don’t need to have productivity as a goal do they? Scale and context applies, could be seen as art even, an expression of someone’s psyche and their world model
iLemming 6mo ago
> you end up with an unproductive culture Practical Lispers would like to have a word - I've been witnessing extreme productivity on some teams. Modern Lisp dialects (Clojure and likes) largely broke library fragmentation and the "not invented here" tendency that were causing real tensions in Common Lisp. You realize that "The Lisp Curse" isn't some paper, survey or objective reflection? It's just someone's essay back from 2011 - an opinion. You can take it word-by-word and apply to say Javascript, and it would largely feel true - JS arguably has the worst fragmentation of any ecosystem; dozens of competing frameworks, build tools, bundlers, test runners; new frameworks constantly replacing old ones; "Javascript fatigue" is a real thing, etc., but nobody talks about "Curse of Javascript" I learned Lisp (once) and that opened up path to Clojure, Clojurescript, then Fennel, Janet and Clojure-Dart, libpython-clj, there's Jank that is about to break loose. And something opposite to fragmentation happened to me - all these incompatible runtimes became unified and controllable from the same substrate - I no longer feel like I'm having to switch between languages - the syntax and thinking stays stable. The runtime is just a deployment target. The curse essay says: "Lisp empowers fragmentation". Actual experience says: "Lisp provides unity across fragmentation that already existed"
- pydry 6mo ago
  >You realize that "The Lisp Curse" isn't some paper, survey or objective reflection? It's just someone's essay back from 2011 - an opinion. It's also the deficit of code we actually use day to day that is actually written in lisp. I file it under the same heading as haskell - a language that clearly has useful ideas, but...
  - ux266478 6mo ago
    You're using Lisp software right now! I think this is the most treacherous assumption people tend to make about programming languages, for a few reasons. One of them is that we really don't have any way to measure software that we actually use day to day. Think about the software controlling your local water treatment plant, traffic lights, the software your local power company relies on, the software running the servers you connect to, and all the servers those things connect to. All the infrastructure in between and the infrastructure's own infrastructure. Allegro Lisp's customers are shotgun spread in industries like healthcare, finance and manufacturing. They're paying for it, so we can infer they're using it, but can anybody actually name what software is written in it? If we play six degrees of separation, accounting for the full gamut of every single computer that does something relevant to your life no matter how distant, how much of that software are you actually familiar with? The fact of the matter is that we genuinely have no broad picture. There is no introspective method to find out what software you are relying on in your day to day life, almost all of it is completely opaque and implicit. To ask "what software do I use?" is to ask an unanswerable question. So to then synthesize an answer is to work with an unsound, unsupported, incomplete conclusion, which is exactly how you end up assuming you don't use software written in Lisp, while directly using software written in Lisp (HN) Of course, even accounting for the epistemic issue, the premise is still flawed. ATS is a language with 'useful ideas, but...', Haskell is an aging pragmatic kitchen sink. Positioning the latter as the former is almost comedic.
yuppiemephisto 6mo ago
https://alok.github.io/assets/lean-position-paper.pdf https://alok.github.io/assets/lean-position-paper.pdf i talked about the lisp curse in this old paper. it's rough but explicitly mentions it

mghackerlady 6mo ago

I can't view the site (Org blocks github for reasons) but I suspect this would be a lot like forth if forth weren't so stack focused

d-us-vb 6mo ago
Forth is at this point more of a culture than a language. It's a culture about keeping designs simple so that they're understandable. Without this, Forth is only powerful for programmers who can keep a lot in their heads, but lots of Forth programs end up being write-once. Moore's view, as well as most other high-level Forthers preach simplicity above all; a code cleanliness that would make Uncle Bob blush. Lean and most type theoretic-based languages don't merely preach simplicity, they demand it. A function or type with a handful of terms or constructors might be provably inhabited/total, whereas one with 2 handfuls of terms or constructors might not be in a reasonable amount of time due to the exponential growth of the proof space. Factoring code optimally for provability yields the simplicity that Forth programmers are striving for.
- blippage 6mo ago
  > Forth is at this point more of a culture than a language. As the saying goes, once you've seen one Forth, then you've seen one Forth. I've mucked around with my own Forths in the past, including one that recognises lexical type, so you could build something like a parser in Forth. I didn't take it that far. Forth is normally conceived as being built from the ground up, but if you're you're going to implement it in C or C++ then you can be more imaginative. I played around with colorforth for 5 minutes on a couple of occasions, but I ran away screaming. What - just what - the hell is going on? I'm sure it all works for Charles Moore, but for mere mortals it might as well be a klingon control panel. I think Moore effectively gave up on programming a couple of years ago? There was some strange modification in the guts of Windows and he couldn't get his environment to work any longer. He concluded that the game was not work the candle.
  - mghackerlady 6mo ago
    One of these days I want to make something forth-y as a shell language. I feel like it could work well there

iLemming 6mo ago

> Homoiconicity anyone? I'm just leaving this here for anyone interested, seems relevant: https://github.com/replikativ/ansatz https://github.com/replikativ/ansatz Ansatz is a verified programming library for Clojure built on the Calculus of Inductive Constructions (CIC) — the same type theory that powers Lean 4.

patrickmay 6mo ago

I came here to comment "We already have Lisp."

DonaldPShimoda 6mo ago

Hm. Homoiconicity is not a well-defined term (see, for example, Shriram Krishnamurthi's thoughts [0][1]), but even skimming over that fact, it is a syntactic property, while the quoted line is about semantics. Switching your language to Lisp (or one of its descendents) doesn't gain you anything semantically. [0] Shriram is an original member of the Racket project, so he's been working in the Lisp-like domain for at least 30 years and, specifically, he works in an offshoot of Lisp that is particularly concerned with questions of syntax. I think this establishes him as a reasonable citation for this topic. [1] https://parentheticallyspeaking.org/articles/bicameral-not-homoiconic/ https://parentheticallyspeaking.org/articles/bicameral-not-h...

noLemming 6mo ago
Well, okay Shriram said the term "homoiconicity" is fuzzy, but the underlying thing (the language of data and the language of programs being the same representation) is real and worth taking seriously. Citing him to wave away the whole concept is pretty wild misuse of the citation. They are refining the claim, not negating it. > doesn't gain anything semantically Syntactic properties create semantic affordances. The reason "code as data" matters isn't that the parentheses look a certain way - it's that the AST is a first-class citizen of the runtime data model. Those are semantic capabilities - they determine what programs can express and compute, especially at the meta level. The syntactic uniformity is the mechanism; the ability to write programs that construct and transform other programs, using the same tools as everything else, is the payoff. Homoiconicity doesn't make Lisp programs mean something different, but it gives you a more uniform and powerful meta-programming model.
- DonaldPShimoda 6mo ago
  > Citing him to wave away the whole concept is pretty wild misuse of the citation. Good thing I didn't do that? > Syntactic properties create semantic affordances. I don't disagree with this. Benjamin Pierce defines type-checking in the opening pages of Types and Programming Languages as an operation over syntax, for example. My point was that the parent comment just kind of threw out "homiconicity" when somebody talked about writing properties about a language in that language, and those are entirely separate things. I was addressing a conflation of terms. The property that people generally refer to as "homoiconicity" is useful for things like writing macros, but it does not directly grant you access to any kind of property-checking capabilitiy. I mean, Rust's macro system is far from homoiconic (it's just an AST), but it gives you semantic capabilities. You know?