A perfectable programming language(alok.github.io)
alok.github.io
A perfectable programming language
https://alok.github.io/lean-pages/perfectable-lean/
151 comments
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-h...
[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-h...
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.
> 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.
> 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?
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?
it's still far easier to write a metainterpreter to play around with language semantics if you have homoiconic syntax. consider the feasibility of altering the search strategy in prolog compared to changing something about c# linq semantics.
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).
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!
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!
I think Idris 2 is targeted more to programming than to doing math, no?
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.
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.
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.
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.
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!
lean IS that language https://github.com/alok/LeanPlot
> 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"
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"
I mostly program with clojure. I'd love that I could agree with you. For clarity I was not meaning a culture of improductivity (but it also applies), and more of a trait of the culture that is improductive, choosing to focus productivity on the wrong goals, such as reinventing everything to do it "better", "more data-driven", "decomplected", etc.
> 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"
You also need to take into account the denominator of "number of users", though. Clojure, with a tiny population, had a cambric explosion of libraries, and now we can't argue that those are dead on one argument, and that those are "done" on the next one. There is a huge fragmentation in the clojure world, and on small populations, that hurts. Case in point: SQL libraries. Korma, yesql, hugsql, honeysql, and those are just the popular ones. Case in point: spec vs. schema vs. malli. Case in point: leiningen vs. boot vs. deps.
> 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.
As we lispers like to say a lot, the syntax (or lack thereof) is the smallest of the issues. There is a lot of semantic difference between all of those (except libpython-clj, which does not belong to that list; but we could add Hy instead). That's even before starting to talk about library compatibility. So I'd contest whether having a common syntax is a major productivity gain.
> 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"
You also need to take into account the denominator of "number of users", though. Clojure, with a tiny population, had a cambric explosion of libraries, and now we can't argue that those are dead on one argument, and that those are "done" on the next one. There is a huge fragmentation in the clojure world, and on small populations, that hurts. Case in point: SQL libraries. Korma, yesql, hugsql, honeysql, and those are just the popular ones. Case in point: spec vs. schema vs. malli. Case in point: leiningen vs. boot vs. deps.
> 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.
As we lispers like to say a lot, the syntax (or lack thereof) is the smallest of the issues. There is a lot of semantic difference between all of those (except libpython-clj, which does not belong to that list; but we could add Hy instead). That's even before starting to talk about library compatibility. So I'd contest whether having a common syntax is a major productivity gain.
I think you're confusing newcomers landscape of "which library do I pick", (which is real) with stretched evidence for fundamentally fragmented ecosystem.
Let's walk through your examples:
SQL libraries: Korma is dead, YeSQL is dead, HugSQL is in maintenance mode. The community converged on next.jdbc + HoneySQL. That's not fragmentation - that's exploration followed by selection.
Build tools: Boot had its moment, it's essentially gone. Leiningen is still around but new projects overwhelmingly use deps.edn. That's not fragmentation either - it's a transition, and a remarkably clean one.
Spec vs. Schema vs. Malli is the most interesting case because the convergence is still in progress. Schema is effectively in maintenance mode. Spec has stalled (spec2 never really shipped). Malli is clearly gaining momentum as the community choice for new work, largely because it treats schemas as data — which is very Clojure. But even here, these aren't competing implementations of the same thing the way, say, Javascript build tools are. They have meaningfully different design philosophies, and the community is converging on the one that best fits Clojure's values.
Compare it to JS, where we have Webpack, Vite, esbuild, Parcel, Rollup, Turbopack, and the "winner" changes every 18 months. Or Python's packaging story - pip, pipenv, poetry, conda, PDM, uv - which is still a mess after decades with a vastly larger community. Fragmentation in large ecosystems often doesn't self-correct because there's enough mass to sustain competing approaches indefinitely.
The small community size that you frame as a weakness is actually why the self-correction works. There aren't enough people to sustain five competing SQL libraries, so the best one wins and everyone moves on. The tight community, the shared values around simplicity and data orientation, and the fact that people actually talk to each other - these create selection pressure that larger, more diffuse ecosystems lack.
The productivity gains aren't speculatory - from the most pragmatic angles, I see time and again - they are real and palpable.
Let's walk through your examples:
SQL libraries: Korma is dead, YeSQL is dead, HugSQL is in maintenance mode. The community converged on next.jdbc + HoneySQL. That's not fragmentation - that's exploration followed by selection.
Build tools: Boot had its moment, it's essentially gone. Leiningen is still around but new projects overwhelmingly use deps.edn. That's not fragmentation either - it's a transition, and a remarkably clean one.
Spec vs. Schema vs. Malli is the most interesting case because the convergence is still in progress. Schema is effectively in maintenance mode. Spec has stalled (spec2 never really shipped). Malli is clearly gaining momentum as the community choice for new work, largely because it treats schemas as data — which is very Clojure. But even here, these aren't competing implementations of the same thing the way, say, Javascript build tools are. They have meaningfully different design philosophies, and the community is converging on the one that best fits Clojure's values.
Compare it to JS, where we have Webpack, Vite, esbuild, Parcel, Rollup, Turbopack, and the "winner" changes every 18 months. Or Python's packaging story - pip, pipenv, poetry, conda, PDM, uv - which is still a mess after decades with a vastly larger community. Fragmentation in large ecosystems often doesn't self-correct because there's enough mass to sustain competing approaches indefinitely.
The small community size that you frame as a weakness is actually why the self-correction works. There aren't enough people to sustain five competing SQL libraries, so the best one wins and everyone moves on. The tight community, the shared values around simplicity and data orientation, and the fact that people actually talk to each other - these create selection pressure that larger, more diffuse ecosystems lack.
The productivity gains aren't speculatory - from the most pragmatic angles, I see time and again - they are real and palpable.
>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...
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...
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.
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.
That's a lot of words to say a lot of FUD.
I know people who work in the embedded space working on stuff similar to traffic lights and LISP isnt even on their radar. Rust is. LISP isnt.
Every niche language has its fanboys who can end up using it all over the place but when it doesnt spread to non fanboys there is usually a reason to which they are wilfully blind, usually related to its practical value.
I know people who work in the embedded space working on stuff similar to traffic lights and LISP isnt even on their radar. Rust is. LISP isnt.
Every niche language has its fanboys who can end up using it all over the place but when it doesnt spread to non fanboys there is usually a reason to which they are wilfully blind, usually related to its practical value.
> Every niche language
Lisp is not a really a programming language. It is an idea.
Lisp didn't emerge the way most languages do - someone sitting down to design syntax and features for practical software engineering. McCarthy was formalizing a notation for computation itself, building on Church's lambda calculus. The fact that it turned out to be implementable was almost a surprise.
And that origin story matters because it explains why Lisp keeps regenerating. Most languages are artifacts - they're designed, they peak, they fossilize. Lisp is more like a principle that keeps getting re-instantiated: Common Lisp, Scheme, Racket, Clojure, Fennel, Jank. Each one is radically different in philosophy and pragmatics, yet they all share something that isn't really about parentheses - it's about code-as-data, minimal syntax hiding maximal abstraction, and the programmer's ability to reshape the language to match the problem rather than the reverse.
The counterargument, of course, is that at some point the idea has to become concrete to be useful, and once it does, it's subject to all the same engineering tradeoffs as any other language. Rich Hickey for example made very specific, opinionated decisions that are engineering choices, not mathematical inevitabilities. So there's a productive tension between Lisp-as-idea and any particular Lisp-as-language.
> related to its practical value.
Don't be daft, preaching pragmatics to modern Lispers is like trying to explain synaptic connections and their plasticity to neurosurgeons. They already know what's what - tis you who's clueless.
Lisp is not a really a programming language. It is an idea.
Lisp didn't emerge the way most languages do - someone sitting down to design syntax and features for practical software engineering. McCarthy was formalizing a notation for computation itself, building on Church's lambda calculus. The fact that it turned out to be implementable was almost a surprise.
And that origin story matters because it explains why Lisp keeps regenerating. Most languages are artifacts - they're designed, they peak, they fossilize. Lisp is more like a principle that keeps getting re-instantiated: Common Lisp, Scheme, Racket, Clojure, Fennel, Jank. Each one is radically different in philosophy and pragmatics, yet they all share something that isn't really about parentheses - it's about code-as-data, minimal syntax hiding maximal abstraction, and the programmer's ability to reshape the language to match the problem rather than the reverse.
The counterargument, of course, is that at some point the idea has to become concrete to be useful, and once it does, it's subject to all the same engineering tradeoffs as any other language. Rich Hickey for example made very specific, opinionated decisions that are engineering choices, not mathematical inevitabilities. So there's a productive tension between Lisp-as-idea and any particular Lisp-as-language.
> related to its practical value.
Don't be daft, preaching pragmatics to modern Lispers is like trying to explain synaptic connections and their plasticity to neurosurgeons. They already know what's what - tis you who's clueless.
You're all over the place here. Yes a chunk of my post is about the epistemic impossibility of knowing what software you rely on. I had to look up what FUD means, I assume it's just an algorithmbrained primitive cognate of epistemic skepticism.
At no point does a post about "You can't draw sweeping conclusions about this kind of thing" imply "all dark matter tech relies on esoteric stacks". I'm not sure why you would even bring up that anecdote?
> there is usually a reason to which they are willfully blind, usually related to its practical value.
Lame passive aggression aside, I'm not a Lisp "fanboy" and I actively don't like the grain of the language. Language adoption is always down to familiarity, taste and ecosystem constraints. But I'm also not deluded enough to assert something like this because I actually know better. It's an argument that's always positioned without substance, because there can be none. You're positioning ignorant snobbishness as enlightened pragmatism, no offense but that's just pretense. If you can't get a Lisp program working on a 100mhz microcontroller with 5k of flash, that's kind of a skill issue dude.
At no point does a post about "You can't draw sweeping conclusions about this kind of thing" imply "all dark matter tech relies on esoteric stacks". I'm not sure why you would even bring up that anecdote?
> there is usually a reason to which they are willfully blind, usually related to its practical value.
Lame passive aggression aside, I'm not a Lisp "fanboy" and I actively don't like the grain of the language. Language adoption is always down to familiarity, taste and ecosystem constraints. But I'm also not deluded enough to assert something like this because I actually know better. It's an argument that's always positioned without substance, because there can be none. You're positioning ignorant snobbishness as enlightened pragmatism, no offense but that's just pretense. If you can't get a Lisp program working on a 100mhz microcontroller with 5k of flash, that's kind of a skill issue dude.
What a thought-terminating cliché. It sounds reasonable while saying nothing. "Useful ideas, but..." what? "But it's not popular"? Neither was Python before it become one. But it doesn't have a big ecosystem? You're describing a consequence of adoption and presenting it as a cause.
Like I said: Clojure runs significant chunks of Walmart's infrastructure, Nubank's entire banking stack serving several hundred million customers - for a second, Nubank is the biggest digital bank in the world; Apple uses it; Cisco uses it. Emacs Lisp runs one of the most enduring pieces of software in computing history. You you ever used Grammarly - it's powered on Lisp; This very site runs on Lisp.
"I don't encounter Lisp in my work and that feels meaningful to me" (there's no other way to interpret your words) is just another, personal opinion that has no practical, objective angle. "The Curse of Lisp" opinion, at least back in the day had some objective relevance that no longer holds true.
Like I said: Clojure runs significant chunks of Walmart's infrastructure, Nubank's entire banking stack serving several hundred million customers - for a second, Nubank is the biggest digital bank in the world; Apple uses it; Cisco uses it. Emacs Lisp runs one of the most enduring pieces of software in computing history. You you ever used Grammarly - it's powered on Lisp; This very site runs on Lisp.
"I don't encounter Lisp in my work and that feels meaningful to me" (there's no other way to interpret your words) is just another, personal opinion that has no practical, objective angle. "The Curse of Lisp" opinion, at least back in the day had some objective relevance that no longer holds true.
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
i talked about the lisp curse in this old paper. it's rough but explicitly mentions it
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
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
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.
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.
> 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.
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.
One of these days I want to make something forth-y as a shell language. I feel like it could work well there
I came here to comment "We already have Lisp."
> Homoiconicity anyone?
I'm just leaving this here for anyone interested, seems relevant: 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.
I'm just leaving this here for anyone interested, seems relevant: 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.
Unfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not care about this anymore.
Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
Also, I dislike that they are using Github as the default package registery. But as this langage was created inside Microsoft, it makes senses.
Lean is far off the most bloated one. Isabelle most likely takes that spot, the main archive includes a whole vscodium among other things.
>> Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three.
> Lean is far off the most bloated one. Isabelle most likely takes that spot.
Among these three is the operative phrase here.
I hate to be pedantic, but we are talking about theorem provers here :)
> Lean is far off the most bloated one. Isabelle most likely takes that spot.
Among these three is the operative phrase here.
I hate to be pedantic, but we are talking about theorem provers here :)
That is a fair point, thank you for the correction there
Static linking wonders?
Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.
Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.
No, it’s still linked dynamically and its kernel is still in C++ (see https://github.com/leanprover/lean4/tree/master/src/kernel, this part of a codebase has hardly changed since Lean 3). Almost all the space in the package (more than 2.5 GiB) is taken up by .olean/.ilean/.ir files, approximately 1 GiB of which is generated from the code of Lean’s frontend itself (i.e., parser, elaborator, core tactics, and so on) and the other 1 GiB from a standard library. As you might guess, these files are IR and essentially a compiled Lean’s environment (something like a Lisp image), so that Lean can load them straight up without recompiling and rechecking everything.
There were some proposals like compressing all the .olean files, but (as far as I know) none of them were implemented. Well, even if some proposals were implemented, their contribution was effectively negated anyway.
There were some proposals like compressing all the .olean files, but (as far as I know) none of them were implemented. Well, even if some proposals were implemented, their contribution was effectively negated anyway.
Thanks for the overview.
i love lean4, best in class functional programming language. but i think its "perfectability" is kinda hamstrung by baking non-constructive axioms into the standard library. the kernel has to treat these as opaque constants that cannot be reduced.
i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.
i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.
Imo F* is a much better choice for proof-oriented programming than lean4. The latter is still largely about mathematics while the former has things like https://fstarlang.github.io/lowstar/html/LowStar.html
Yes, a strong argument, and staying in a line of PLs: F# for high-level, and F* <-> Low* for theorem proving and low-level coding. I am evaluating F/Low for verified code on Cortex M processor that I am currently trying to write SPARK2014. The Cortex A processor is running seL4 for less safety-critical tasks. I did look at Lean4 as a scratch for my Idris2 itch use cases.
this is the log post that put lean on my radar, though I haven't played with it yet: https://kirancodes.me/posts/log-ocaml-to-lean.html
Great post. Thanks!
Fortran, Basic, APL, Beta, Odin, Self, C, C++, Objective-C, C#, C--, D, Scheme, Clojure, F-Script, Eiffel, COBOL, Ocaml, Haskell, Snobol, Crystal, Forth, Python, Lisp, Brainfuck, Java, Oak, Javascript, TypeScript, Wasm, Logo, Elang, Elixir, Gleam, Elm, Zig, m4, Tcl, Simula, Smalltalk
Fun challenge. Unlike the author, I have nothing really to add.
I just wanted to say that "I did NOT write it with ..."
Fun challenge. Unlike the author, I have nothing really to add.
I just wanted to say that "I did NOT write it with ..."
Indeed! I got to about 20 with A-B-C but it somehow became harder after those. The multitude of C-something is obvious but I didn't realize there's so many A* languages (apl, ada, agda, alice, algol, applescript, apex, ampl, assembly..)
Then there’s the actual language ABC. It’s in the Basic family and has whitespace indentation for structuring flow. It directly influenced Python.
You could start your list alphabetically with A, A+, and A++. A is derived from APL. A+ is a newer take on A. A++ is unrelated. https://a-plus-plus-devs.github.io/aplusplus/guide/getting-s...
You could start your list alphabetically with A, A+, and A++. A is derived from APL. A+ is a newer take on A. A++ is unrelated. https://a-plus-plus-devs.github.io/aplusplus/guide/getting-s...
C--! I forgot that one. The ILR for the first versions of the Glasgow Haskell Compiler
Are they actual project running some business in the wild? I only played with coq in university, while I saw F# being employed in insurance companies. I only heard about lean through HN posts.
I don't know about running per se but practical applications (as in done for product/service) exist. A notable practitioner for Isabelle and Lean is AWS[0]. There is also TLA+ for a more practical tool.
The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation.
[0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.... and https://lean-lang.org/ (Cedar)
The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation.
[0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.... and https://lean-lang.org/ (Cedar)
I've been messing around with a computer algebra simplifier in Lean:
https://github.com/dharmatech/symbolism.lean
Lean is astonishingly expressive.
https://github.com/dharmatech/symbolism.lean
Lean is astonishingly expressive.
i like this website, it shows documentation when hovering the code while i see similar stuffs really rare in web blog areas
I believe you can thank Verso for that:
https://github.com/leanprover/verso
https://github.com/leanprover/verso
> the easiest way to do anything is properly.
Oh, what a beautiful world it would be if this were the case!
Oh, what a beautiful world it would be if this were the case!
[deleted]
[deleted]
[deleted]
> at a party, Sydney Von Arx asked if i could name 40 programming languages.
An attempt (without looking)
JavaScript QBasic PHP Haskell C C++ Ada Algol Racket Scheme Clojure Common-Lisp GOOL Fortran Awk Postscript Forth C# F# Lua Java D Odin Rust Zig Julia Python Nim MATLAB Bash Brainfuck Arnold-C Intercal Gleam Unison Ruby Crystal Erlang Go TCL
Phew!
An attempt (without looking)
JavaScript QBasic PHP Haskell C C++ Ada Algol Racket Scheme Clojure Common-Lisp GOOL Fortran Awk Postscript Forth C# F# Lua Java D Odin Rust Zig Julia Python Nim MATLAB Bash Brainfuck Arnold-C Intercal Gleam Unison Ruby Crystal Erlang Go TCL
Phew!
It's a fun challenge! My list is Ada Agda Assembly Awk BASIC Brainfuck C C# C++ COBOL Curry D Elixir Elm F# FORTRAN Gleam GLSL Go Haskell HCL Idris Intercal Java Javascript Objective-C Ocaml Pascal Pony Prolog Python R Ruby Rust Sh Sketch Swift Typescript Visual Basic Zig
Hahaha I very much enjoyed seeing GOOL there. I also love that you went for that over GOAL, which is probably the much more famous one.
XL is a very interesting modern iteration on extensible languages, unfortunately it seems abandoned.
I don't usually like to appeal to authority but this time it's too "perfect".
"There are only two kinds of languages: the ones people complain about and the ones nobody uses". - Bjarne Stroustrup
"There are only two kinds of languages: the ones people complain about and the ones nobody uses". - Bjarne Stroustrup
> languages without types tend to grow them, like PHP in 7.4 and Python type annotations
Well ... that is a trend that is driven largely by people who love types.
Not everyone shares that opinion. See ruby.
It is very hard to try to argue with people who love types. They will always focus on "types are great, every language must have them". They, in general, do not acknowledge trade-offs when it comes to type systems.
So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types. I saw this happen "live" in ruby; I am certain this happened in python too.
> inevitably, people want to push types. even Go. C++ templates are the ultimate example. if it can be computed at compile time, at some point someone wants to, like Rust's ongoing constification.
And many people hate C++ templates. But comparing that language to e. g. ruby is already a losing argument. Languages are different. So are the trade-offs.
> dependent types can get you there. hence perfectable.
So the whole point about claiming a language is "perfectable", means to have types? I don't agree with that definition at all.
> most languages have no facility for this,
How about lisp?
> this lets you design APIs in layers and hide them behind syntax.
The language already failed hard syntax-wise. This is a problem I see in many languages - 99% of the language designers don't think syntax is important. Syntax is not the most important thing in the world, but to neglect it also shows a lack of understanding why syntax ALSO matters. But you can not talk about that really - I am 100% certain alok would disagree. How many people use a language also matters a LOT - you get a lot more momentum when there are tons of people using a language, as opposed to the global 3 or 4 using "lean".
Well ... that is a trend that is driven largely by people who love types.
Not everyone shares that opinion. See ruby.
It is very hard to try to argue with people who love types. They will always focus on "types are great, every language must have them". They, in general, do not acknowledge trade-offs when it comes to type systems.
So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types. I saw this happen "live" in ruby; I am certain this happened in python too.
> inevitably, people want to push types. even Go. C++ templates are the ultimate example. if it can be computed at compile time, at some point someone wants to, like Rust's ongoing constification.
And many people hate C++ templates. But comparing that language to e. g. ruby is already a losing argument. Languages are different. So are the trade-offs.
> dependent types can get you there. hence perfectable.
So the whole point about claiming a language is "perfectable", means to have types? I don't agree with that definition at all.
> most languages have no facility for this,
How about lisp?
> this lets you design APIs in layers and hide them behind syntax.
The language already failed hard syntax-wise. This is a problem I see in many languages - 99% of the language designers don't think syntax is important. Syntax is not the most important thing in the world, but to neglect it also shows a lack of understanding why syntax ALSO matters. But you can not talk about that really - I am 100% certain alok would disagree. How many people use a language also matters a LOT - you get a lot more momentum when there are tons of people using a language, as opposed to the global 3 or 4 using "lean".
You mentioned there are reasons not to type check your program. I would very much like to hear what they are!
Also, I have to point out that of course Ruby has types. And it does type checking. It just does it when the line of code actually runs. (i.e. runtime type errors).
So the discussion here isn't should we check types or not. It's a question of when to do it.
Do you want to know you've made a mistake when you actually make it? Or do you want to find out an unknown amount of time later (e.g. in unfortunate cases, several months later, debugging an issue in prod. Not that I would know anything about that ;)
---
My own thinking on the subject is that it should be configurable.
Rust's level of correctness, for example is probably overkill for a game jam. (As is, arguably, using a low level language in the first place.)
But my thinking here is that correctness should be opt out rather than opt-in. If you have a good reason to make your program wrong by default, then you should be allowed to do that. But it should be a conscious choice! And every source file, at the top of the file, should remind you that you are making that choice: #JAMMODE
And if you intend to actually ship the thing, and charge money for it, in Serious Release Mode the compiler should refuse to build anything that's still in jam mode.
My point here is that some languages make jam mode the only option you have.
Also, I have to point out that of course Ruby has types. And it does type checking. It just does it when the line of code actually runs. (i.e. runtime type errors).
So the discussion here isn't should we check types or not. It's a question of when to do it.
Do you want to know you've made a mistake when you actually make it? Or do you want to find out an unknown amount of time later (e.g. in unfortunate cases, several months later, debugging an issue in prod. Not that I would know anything about that ;)
---
My own thinking on the subject is that it should be configurable.
Rust's level of correctness, for example is probably overkill for a game jam. (As is, arguably, using a low level language in the first place.)
But my thinking here is that correctness should be opt out rather than opt-in. If you have a good reason to make your program wrong by default, then you should be allowed to do that. But it should be a conscious choice! And every source file, at the top of the file, should remind you that you are making that choice: #JAMMODE
And if you intend to actually ship the thing, and charge money for it, in Serious Release Mode the compiler should refuse to build anything that's still in jam mode.
My point here is that some languages make jam mode the only option you have.
> So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types.
Who else would add them, besides people who want them? I'm confused about what you're even claiming here. It sounds like you feel that there's a vocal minority of type enthusiasts who everyone else is just humoring by letting them bolt on their type systems.
Who else would add them, besides people who want them? I'm confused about what you're even claiming here. It sounds like you feel that there's a vocal minority of type enthusiasts who everyone else is just humoring by letting them bolt on their type systems.
Well Ruby kinda brought forth Crystal which while its own Programming Language is kinda Ruby but with Types.
Here's a recent talk about how "concrete syntax matters, actually": https://www.youtube.com/watch?v=kQjrcSMYpaA
Highly recommended!
Highly recommended!
actually i think syntax is incredibly important, but i think i'm approaching it from a viewpoint that's even more syntactic than lisp macros, which in practice tend to center around parens syntactically still. racket a notable exception (and good, but not perfectable lang, one of the inspirations for my remark). typed racket is good but is not culturally central enough. but yeah, i do believe types are [inevitable](https://www.youtube.com/watch?v=0AQdSZqGXz4)
https://reservoir.lean-lang.org/@strata-org/Strata isn't done, but its goal is to let one build whole languages that can look like whatever you like. ones for little kids maybe
syntax matters for normal ppl even more than semantics in some ways since semantics can be optimized and refined on the backend, but everyone is (de)limited by their vocabulary
https://reservoir.lean-lang.org/@strata-org/Strata isn't done, but its goal is to let one build whole languages that can look like whatever you like. ones for little kids maybe
syntax matters for normal ppl even more than semantics in some ways since semantics can be optimized and refined on the backend, but everyone is (de)limited by their vocabulary
> do not acknowledge trade-offs when it comes to type systems
Could you elaborate?
Could you elaborate?
Here's a good summary of the limited evidence for the benefits of strong type systems: https://danluu.com/empirical-pl/
> do not acknowledge trade-offs when it comes to type systems
> gives link to "limited evidence of benefits"
I'm not looking for absence of evidence, as absence of evidence does not mean evidence of absence. The original post claims tradeoffs, where are they? What are we trading? Even the most dynamic-language friendly results in your linked post either claim: "look at what we did without types!" or "even though there's no types in ruby, devs think about them all the time", which I mean, come on.
The only real criticism or tradeoffs on types mentioned is a person getting stuck on a single static type check compilation error, but I can easily counter that with "undefined is not a property of null".
From the link:
> if the strongest statement you can make for your position is that there's no empirical evidence against the position, that's not much of a position.
This is how hypotheses work. Maybe the problem is that we have a hard time proving anything about programming languages?
> gives link to "limited evidence of benefits"
I'm not looking for absence of evidence, as absence of evidence does not mean evidence of absence. The original post claims tradeoffs, where are they? What are we trading? Even the most dynamic-language friendly results in your linked post either claim: "look at what we did without types!" or "even though there's no types in ruby, devs think about them all the time", which I mean, come on.
The only real criticism or tradeoffs on types mentioned is a person getting stuck on a single static type check compilation error, but I can easily counter that with "undefined is not a property of null".
From the link:
> if the strongest statement you can make for your position is that there's no empirical evidence against the position, that's not much of a position.
This is how hypotheses work. Maybe the problem is that we have a hard time proving anything about programming languages?
> > languages without types tend to grow them, like PHP in 7.4 and Python type annotations
...
> Not everyone shares that opinion. See ruby.
All programming languages that have values (i.e. all of them) have types, because you cannot have a concrete value that doesn't have a type. This includes Ruby.
The only difference is whether the language lets you annotate the source code with the expected type of each value.
This is why you observe that all languages trend towards visible typing: The types are already there and it's only a matter of whether the language lets the programmer see it, or lets a linter enforce it, and everyone likes linters.
> So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types.
Maybe you misidentified where the type declaration is coming from? It might not be coming from people who want to see types in the source code, it most probably is coming from people who want a decent linter.
In 2026, programming without type-enforcement is like programming using an LLM; it's quicker, but less safe.
...
> Not everyone shares that opinion. See ruby.
All programming languages that have values (i.e. all of them) have types, because you cannot have a concrete value that doesn't have a type. This includes Ruby.
The only difference is whether the language lets you annotate the source code with the expected type of each value.
This is why you observe that all languages trend towards visible typing: The types are already there and it's only a matter of whether the language lets the programmer see it, or lets a linter enforce it, and everyone likes linters.
> So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types.
Maybe you misidentified where the type declaration is coming from? It might not be coming from people who want to see types in the source code, it most probably is coming from people who want a decent linter.
In 2026, programming without type-enforcement is like programming using an LLM; it's quicker, but less safe.
I also add the observation that while the dynamic typing languages are all growing in the direction of the statically-typed languages, no statically-typed language (that I know of) is adding a lot of dynamically-typed features. If anything the static languages trend towards more static typing. Which doesn't mean the optimum is necessarily "100% in the direction of static typing", the costs of more static typing do eventually overwhelm the benefits by almost any standard, but the trend is universal and fairly clear.
I kind of think there's room for a new dynamically-typed language that is designed around being fast to execute and doesn't cost such a huge performance multiple right off the top, and starts from day 1 to be multi-thread capable, but on the whole the trend is clearly in the direction of static typing.
I kind of think there's room for a new dynamically-typed language that is designed around being fast to execute and doesn't cost such a huge performance multiple right off the top, and starts from day 1 to be multi-thread capable, but on the whole the trend is clearly in the direction of static typing.
> I kind of think there's room for a new dynamically-typed language that is designed around being fast to execute and doesn't cost such a huge performance multiple right off the top, and starts from day 1 to be multi-thread capable, but on the whole the trend is clearly in the direction of static typing.
Other than the "new" qualifier, Lisp supports all of that - SBCL compiles to native code, ecl/gcl compile to C (IIRC), etc.
Other than the "new" qualifier, Lisp supports all of that - SBCL compiles to native code, ecl/gcl compile to C (IIRC), etc.
Some languages have only a single type, e.g. BrainFuck only has "byte". Shells tend to only have "string" as a fundamental type, and some helpers to do things like split strings on a separator & iterate over the elements or to treat strings as numbers to do arithmetic. Such single-type languages tend to be esoteric and/or difficult to program in, since every sort of data manipulation not supported by that type has to be done at runtime, by the programmer.
> Such single-type languages tend to be esoteric and/or difficult to program in, since every sort of data manipulation not supported by that type has to be done at runtime, by the programmer.
It depends; I recall programming in Tcl in the late 90s, and that has only the string and the list as datatypes, but it felt very powerful, like Lisp but without the easy syntax.
It depends; I recall programming in Tcl in the late 90s, and that has only the string and the list as datatypes, but it felt very powerful, like Lisp but without the easy syntax.
Powerful, yes. Easy to program in, no.
> How about lisp?
I was wondering why lisp (and forth) were omitted from the initial list of languages named in the post.
I guess Scheme is in the list has ok macros.
I was wondering why lisp (and forth) were omitted from the initial list of languages named in the post.
I guess Scheme is in the list has ok macros.
I get adding Scheme, but omitting CL seems like a big oversight
For anyone as curious as me, here's short description for each language in the list (excluding most common ones):
cyclone: safe C dialect preventing memory errors
zig: modern systems language with explicit control over memory
odin: another modern systems language
nim: Python-like syntax, memory safe, compiles to C/C++/JS
visual basic: event-driven language for Windows GUI apps
actionscript: language for Adobe Flash applications
php: server-side scripting for web development
typescript: JavaScript with static types
elm: functional language that compiles to JS, no runtime errors
purescript: Haskell-like language compiling to JS
haskell: purely functional, lazy language with strong types
agda: dependently typed functional language for theorem proving
idris: dependently typed language for type-driven development
coq: proof assistant based on Calculus of Inductive Constructions
isabelle: interactive theorem prover
clean: purely functional language with uniqueness typing
unison: content-addressed functional language with hashes instead of names
scheme: minimalist Lisp dialect used in academia
racket: a Scheme/Lisp dialect for language-oriented programming
prolog: logic programming with backtracking
ASP: Answer Set Programming for combinatorial search
clingo: ASP solver for logic-based reasoning
zsh: extended Bourne shell with advanced scripting
tcsh: enhanced C shell with command-line editing
awk: pattern-directed text processing language
sed: stream editor for text transformation
hack: PHP-derived language with gradual typing
verilog: hardware description language for digital circuits
whitespace: esoteric language using only spaces, tabs, newlines
intercal: esoteric language designed to be confusing
alokscript: can't find anything =(> scheme: minimalist Lisp dialect used in academia
There are very minimal versions and also huge versions with lot of libraries, batteries and the kitchen sink.
There are very minimal versions and also huge versions with lot of libraries, batteries and the kitchen sink.
The author is named Alok, so I would expect alokscript to be a self-authored programming language. But I checked the GitHub profile and I don't see anything.
i was just messing with you guys, but now i'm feeling a bit more motivated
[deleted]
The perfect programming language has:
- The compile speed of Go
- The performance of Go
- The single binary compilation of Go
- The type system of Kotlin
- The ecosystem of JVM (packages for anything I could dream of)
- The document sytem/tests of Elixir
- The ability to go "unsafe" and opt for ARC instead of GC
- The result monad/option monad and match statements from OCaml/Gleam
- A REPL like Kotlin or even better, OCaml
- A GREAT LSP for NeoVim
- A package/module system that minimizes transient dependencies
- No reliance on a VM like BEAM or JVM
Common Lisp through SBCL fits this for everything but changing GC strategies. I'm not sure why you'd do that, though. SBCL's generational GC is faster in all cases, easy to reason about, and trivial to pause.
In many of these other categories, clisp exceeds requirements. The REPL and Doc situation is so good it's honestly worth it for those alone. People put up with `):'(,@ soup for good reason.
In many of these other categories, clisp exceeds requirements. The REPL and Doc situation is so good it's honestly worth it for those alone. People put up with `):'(,@ soup for good reason.
I luckily have the freedom to work with SBCL almost fulltime. It is a joy; shame most will never get to experience it (few jobs, parenthophobia etc).
Alright, you and your sibling reply have me wanting to look at it. I wrote Scheme/Racket when I was going through The Little Schemer and SICP. I'll buy a common lisp book. Any recommendations?
Common Lisp Is exactly that. I wish I could use it at work. All my personal stuff nowadays is CL only. There is no other choice.
I believe there are tradeoffs which is why this doesn't exist. Isn't the compile speed of Go so good because it's type system is much simpler?
Yes, programming languages are designed for a purpose and importantly for a concrete system. Erlang is the way it is because it was designed for Ericsson's phone network. C is the way it is because it was designed for the PDP-11. Logo is the way it is because is was designed for young children. Go is they way it is because it was designed by Google for Googlers.
You can't design an abstractly "perfect" programming language without any context. Which is why the author I think focuses on "perfectable", as in the language can be made perfect for your purpose but it's not going to be one size fits all.
You can't design an abstractly "perfect" programming language without any context. Which is why the author I think focuses on "perfectable", as in the language can be made perfect for your purpose but it's not going to be one size fits all.
No, I realize that. It doesn't stop me from having my "perfect language wishlist". The author calling out "perfectable" is what got me thinking. What language would I choose if I were able to "perfect" it just a bit more?
But you had called your list "one size fits all".
...in an imaginary world where we're still writing code, yes. It's a musing, not a directive.
One thing I like about TypeScript is that there's tooling for "quickly strip out the types and give me something I can run; I don't care if it's correct". You can run the (slower) type checker concurrently with that (or whenever it's convenient to do so), but type-checking doesn't necessarily block you from being able to play with runtime stuff.
I understand that this workflow can't be realized in languages whose runtime semantics are derived from type-level stuff, and while that can be quite convenient I'm personally willing to give it up to unlock the aforementioned workflow.
I understand that this workflow can't be realized in languages whose runtime semantics are derived from type-level stuff, and while that can be quite convenient I'm personally willing to give it up to unlock the aforementioned workflow.
"Isn't the compile speed of Go so good because it's type system is much simpler?"
That, and forgoing fancy compile-time optimization steps which can get arbitrarily expensive. You can recover some of this with profile-guided optimization, but only some and my best guess based on the numbers is that it's not much compared to a more full (but much more expensive) suite of compile-time optimizations.
That, and forgoing fancy compile-time optimization steps which can get arbitrarily expensive. You can recover some of this with profile-guided optimization, but only some and my best guess based on the numbers is that it's not much compared to a more full (but much more expensive) suite of compile-time optimizations.
oh yeah absolutely. The moment you start blowing up Go with features (for example) the speed decreases dramatically.
"The compile speed of Go" - Delphi starts laughing
performance of Go - why not Fortran?
type system of Kotlin - why not Scala/Haskell?
Repl like Kotlin, why not Clojure?
> The result monad/option monad and match statements from OCaml/Gleam
Do you mean actual monads or just the specific result/option containers? If you mean a fully-fledged monad abstraction then you need a more sophisticated type system than what Kotlin provides (i.e. higher-kinded types).
Do you mean actual monads or just the specific result/option containers? If you mean a fully-fledged monad abstraction then you need a more sophisticated type system than what Kotlin provides (i.e. higher-kinded types).
Kotlin itself has opted for inline union types to represent error results: https://github.com/Kotlin/KEEP/blob/main/proposals/KEEP-0441...
The existing Result type was a mistake to expose to users, IMO, as it encourages exceptions-as-control-flow and error type hierarchies which complicate error-handling even further. The convenient `runCatching` API also completely breaks reasonable error-handling on the JVM and Kotlin's structured concurrency (which happens to use exceptions-as-control-flow to signal coroutine cancellation).
Overall, Kotlin is moving away from higher-kinded types in the core language, not toward them.
The existing Result type was a mistake to expose to users, IMO, as it encourages exceptions-as-control-flow and error type hierarchies which complicate error-handling even further. The convenient `runCatching` API also completely breaks reasonable error-handling on the JVM and Kotlin's structured concurrency (which happens to use exceptions-as-control-flow to signal coroutine cancellation).
Overall, Kotlin is moving away from higher-kinded types in the core language, not toward them.
I'm not a frequent Kotlin user but none of that surprises me. My comment was asking about nobleach's imaginary "perfect programming language", which is clearly not Kotlin.
I'd settle for the Result/Option containers. Kotlin does have ArrowKt to attempt to achieve all the functional goodness of Scala. I think for my needs though, I'd appreciate Rust's "Result".
What do you like so much about Kotlin type system, and document / testing of elixir?
The type system of Kotlin? It's the same as Java + syntactic sugar for nullability. Don't pretend otherwise.
- The reach of JavaScript
[deleted]
Very nice!
I've been wanting to adopt Lean for a project but wasn't sure about the speed. Nice to hear that it should be good on that front.
I've been wanting to adopt Lean for a project but wasn't sure about the speed. Nice to hear that it should be good on that front.
> For Eliza Zhang, who bet I couldn’t write a web app in C in one week using only the standard library. She was right. I didn’t know what any of those words meant. But I said the fuck I can’t, and that’s how I got into coding.
interesting the ones they chose to name; I would have probably started with 6502/68000/68020/z80 assembly, fortran, cobol, basic, c, ada, simula 67, sh, zsh, bash, napier 88, tcl, perl, rexx, before hitting the next generation of python, c++, etc.
fwiw, I think a similar tik-tac-toe evaluator could be made in rust declarative macros, no proc macros needed. I’ll see if I can smuggle some experimentation time today to make an example.
Very intersting, never heard of lean before tbh
wait, I'm intrigued, it says the blog itself is lean code. How? It's rendered, like pollen?
It is verso. My understanding is that it's like really fancy javadocs that makes communicating Lean code easier for everyone.
https://github.com/leanprover/verso
https://github.com/leanprover/verso
The thing I found really surprising about Lean is that although it is really focused on proving stuff, it has some surprisingly enormous footguns. What do you think the result of these are?
Nope! Both give 0.
#eval (UInt8.ofNat 256 : UInt8)
#eval (4 - 5 : Nat)
Nope! Both give 0.
Who said that it should be a compile time error? That’s just a convention, and this is definitely not a bad one. No one is going to like the need to pass each time a proof that `a ≥ b` for every `a - b` invocation. Taking into account that this proof will most likely be an implicit argument, that would be a really annoying thing to use.
On the other hand, array indices by default do require such a proof, i.e., this code produces a compile time error:
On the other hand, array indices by default do require such a proof, i.e., this code produces a compile time error:
def x := #[1, 2, 3, 4]
#check x[7]
> this is definitely not a bad one
It definitely is a bad convention because it's highly surprising. That's what makes it a footgun.
> that would be a really annoying thing to use
Sure. So maybe provide "unchecked" versions for when people don't want to bother.
We've known this about interface design for literally decades. The default must be safe and unsurprising. You need to opt into unsafety.
It definitely is a bad convention because it's highly surprising. That's what makes it a footgun.
> that would be a really annoying thing to use
Sure. So maybe provide "unchecked" versions for when people don't want to bother.
We've known this about interface design for literally decades. The default must be safe and unsurprising. You need to opt into unsafety.
>It definitely is a bad convention because it's highly surprising.
You know that `Nat` represents non-negative numbers, and you see that `1 - 2` does not produce a compile error. What value do you expect then? What’s so surprising about choosing zero as a default value here? Do you expect it to panic or what?
You know that `Nat` represents non-negative numbers, and you see that `1 - 2` does not produce a compile error. What value do you expect then? What’s so surprising about choosing zero as a default value here? Do you expect it to panic or what?
I would expect it to require a proof that 1 - 2 is non-negative. That's kind of the raison d'etre of Lean isn't it?
The reason they don't do that is because Lean treats proofs as manually generated explicit objects, unlike other languages like Dafny (IIRC) where they are implicit. Requiring explicit proofs for every subtraction was presumably seen as too onerous.
Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".
If they had used something like 1 -_ 2 then that would be much less surprising because you'd think "oh right, it's the special saturating subtraction".
Similarly for Uint8.ofNat it should have been Uint8.ofNatWrapping or similar.
This shouldn't be news.
The reason they don't do that is because Lean treats proofs as manually generated explicit objects, unlike other languages like Dafny (IIRC) where they are implicit. Requiring explicit proofs for every subtraction was presumably seen as too onerous.
Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".
If they had used something like 1 -_ 2 then that would be much less surprising because you'd think "oh right, it's the special saturating subtraction".
Similarly for Uint8.ofNat it should have been Uint8.ofNatWrapping or similar.
This shouldn't be news.
>I would expect it to require a proof that 1 - 2 is non-negative. That's kind of the raison d'etre of Lean isn't it?
The reason is to be able to write mathematical proofs, including proofs about your code, but not to attach proofs to every single function. This definition of subtraction does not prevent you from reasoning about it and requiring `a ≥ b` in the proofs/code for which this is really important.
>Requiring explicit proofs for every subtraction was presumably seen as too onerous.
Lean can deduce proofs implicitly as well. It’s just not a very reliable mechanism. That is, imagine your code breaking after an update, because Lean suddenly can’t deduce `a ≥ b` automatically for you anymore.
>Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".
What is a standard subtraction over natural numbers at all? As you know, under a standard addition natural numbers form a monoid but not a group.
The reason is to be able to write mathematical proofs, including proofs about your code, but not to attach proofs to every single function. This definition of subtraction does not prevent you from reasoning about it and requiring `a ≥ b` in the proofs/code for which this is really important.
>Requiring explicit proofs for every subtraction was presumably seen as too onerous.
Lean can deduce proofs implicitly as well. It’s just not a very reliable mechanism. That is, imagine your code breaking after an update, because Lean suddenly can’t deduce `a ≥ b` automatically for you anymore.
>Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".
What is a standard subtraction over natural numbers at all? As you know, under a standard addition natural numbers form a monoid but not a group.
> Lean can deduce proofs implicitly as well.
Sure, but you still have to explicitly ask it to.
> What is a standard subtraction over natural numbers at all?
If you need something that is always defined then you have to use a non-standard subtraction (i.e. saturating subtraction). In other words the `-` operator should not work for Nat. It should require you to use `-_`.
Sure, but you still have to explicitly ask it to.
> What is a standard subtraction over natural numbers at all?
If you need something that is always defined then you have to use a non-standard subtraction (i.e. saturating subtraction). In other words the `-` operator should not work for Nat. It should require you to use `-_`.
i agree about this point, i think this is one of the ways extensible syntax can save (or damn, like in this case) you
These are both pretty reasonable semantics for these functions. `UInt8.ofNat : Nat -> UInt8` might reasonably map the infinite number of `Nat` values to `UInt8` by taking the natural number modulo 256. And it's sensible enough that subtraction with natural numbers should saturate at 0.
These aren't the only reasonable semantics, and Lean will certainly let you define (for instance) a subtraction function on natural numbers that requires that the first argument is greater than or equal to the second argument, and fail at compile time if you don't provide a proof of this. These semantics do have the benefit of being total, and avoiding having to introduce additional proofs or deal with modeling errors with an `Except` type.
These aren't the only reasonable semantics, and Lean will certainly let you define (for instance) a subtraction function on natural numbers that requires that the first argument is greater than or equal to the second argument, and fail at compile time if you don't provide a proof of this. These semantics do have the benefit of being total, and avoiding having to introduce additional proofs or deal with modeling errors with an `Except` type.
Good point, and an important example why static types are ultimately a failure: Encoding the actual invariants in them you care about is a pain in the ass.
No doubt there will be plenty of comments to your comment trying to rationalise this.
No doubt there will be plenty of comments to your comment trying to rationalise this.
Why do you believe that static types are ultimately a failure?
I strongly disagree. Static types are a huge success. The problem here is essentially that they named things badly.
Better than simply not encoding the actual invariants you care about.
body { max-width: 70rem; }
A very polite reminder that Elixir exists.
>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension,
Lol
Lol
There are community-built editor supports. For example,
- Emacs: https://github.com/leanprover-community/lean4-mode
- Neovim: https://github.com/Julian/lean.nvim
I'm using the Emacs lean4-mode and it's pretty good.
- Emacs: https://github.com/leanprover-community/lean4-mode
- Neovim: https://github.com/Julian/lean.nvim
I'm using the Emacs lean4-mode and it's pretty good.
It makes complete sense to polish that usecase.
What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
Wow, I read the whole thing without noticing that.
But as someone who came of age in the AIM / ICQ / IRC days, it feels pretty normal. That's just how we wrote. I still fall into it by accident when the context is right and I'm not thinking about it (eg Slack at work). I hope youngsters aren't judging me for it.
But as someone who came of age in the AIM / ICQ / IRC days, it feels pretty normal. That's just how we wrote. I still fall into it by accident when the context is right and I'm not thinking about it (eg Slack at work). I hope youngsters aren't judging me for it.
we wrote like that because each message was a single sentence
if you wanted more than one sentence you sent one then wrote the other
it's painful to read longform
the victorians didn't give up on punctuation and regular english just because they had the telegraph
if you wanted more than one sentence you sent one then wrote the other
it's painful to read longform
the victorians didn't give up on punctuation and regular english just because they had the telegraph
I think this is just applying the same informal writing style used in, for example, online chats with friends, to a relatively-informal blog post. I don't think this has anything to do with the Bay Area or its tech industry in particular.
[deleted]
YES, THIS (capitalized on purpose). Folks, please use reasonably correct writing syntax. You CAN do better .. At least think of the AIs consuming your writings.
I ReSpEcTfUlLy DiSaGrEe FrIeNd -- PeOpLe LoVe SlOp. =3
its not caused by a habit of writing authentically formatted Homestuck rp smut
but surely its correlated
but surely its correlated
It communicates a certain tone that is sometimes what one is going for. I do it in HN comments sometimes if I'm feeling, like, dry or dismissive.
Is it due to the feature that the author claimed "this blog post is itself Lean code"?
some combo of implicit pride and laziness. sorry, i'll fix it up
It’s to show you’re too cool for grammar rules.
i notoriously ignore using my shift key when im typing informal stuff (comments, chats to coworkers, friends, etc). big ol emails = you'll see me using my shift key.
most of this comes from me noticing how funny sql looks with all the people trying to use caps all over the place as if anyones working in a place without syntax highlighting in 2026. sql is the wild west and everyones sql looks like shit there is no shame. i was told i needed to use caps more early on in sql and i lmfao'd, but i was new to the career and that scarred me. i write lower case sql just to spite others now and if you see something capitalized you know i meant it, but for the most part you have to pay me to use my shift key.
my trauma is now your trauma
most of this comes from me noticing how funny sql looks with all the people trying to use caps all over the place as if anyones working in a place without syntax highlighting in 2026. sql is the wild west and everyones sql looks like shit there is no shame. i was told i needed to use caps more early on in sql and i lmfao'd, but i was new to the career and that scarred me. i write lower case sql just to spite others now and if you see something capitalized you know i meant it, but for the most part you have to pay me to use my shift key.
my trauma is now your trauma
Only you can stop generational SQL abuse. Capitalize keywords, indent grouped syntax, and use prefix commas on newlines. Write readable code, for God’s sake, you filthy heathens.
The swearing is another thing I keep seeing more of.
clojure exists as an example of people trying types and then realising it's cruft and not needed.
Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.