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.
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!
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.
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.
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.
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
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.
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.
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.
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.
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.
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.
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..)
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 =(
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.
- 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
I still dream about this "one size fits all" language.
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.
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.
"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.
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.
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?
> 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).
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.
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.
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.
> 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.
> 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".
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.
> 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.
> > 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.
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.
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.
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?
The first should be a compile time error right, because `UInt8.ofNat` is going to require that its argument is 0-255. And the second should be a compile time error because subtraction should not give a `Nat` unless the first argument is definitely more than the second.
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:
>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?
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.
>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.
> 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 `-_`.
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.
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.
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.
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.
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 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.
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.
> 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.
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...
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!
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.
> 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"
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 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...
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.
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.
> 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 came here to comment "We already have Lisp."
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.
Also, I dislike that they are using Github as the default package registery. But as this langage was created inside Microsoft, it makes senses.
The name is amusingly ironic now.
Static linking wonders?
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.
Thanks for the overview.
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 :)
That is a fair point, thank you for the correction there
> 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!
> the easiest way to do anything is properly.
Oh, what a beautiful world it would be if this were the case!
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.
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.
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)
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 ..."
C--! I forgot that one. The ILR for the first versions of the Glasgow Haskell Compiler
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...
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!
I've been messing around with a computer algebra simplifier in Lean:
https://github.com/dharmatech/symbolism.lean
Lean is astonishingly expressive.
For anyone as curious as me, here's short description for each language in the list (excluding most common ones):
> 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.
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.
XL is a very interesting modern iteration on extensible languages, unfortunately it seems abandoned.
The perfect programming language has:
I still dream about this "one size fits all" language.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.
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 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).
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?
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.
"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.
oh yeah absolutely. The moment you start blowing up Go with features (for example) the speed decreases dramatically.
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.
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".
What do you like so much about Kotlin type system, and document / testing of elixir?
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).
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.
[delayed]
"The compile speed of Go" - Delphi starts laughing
- The reach of JavaScript
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
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 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.
Very intersting, never heard of lean before tbh
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.
> 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.
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
A very polite reminder that Elixir exists.
> 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".
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.
> 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.
> do not acknowledge trade-offs when it comes to type systems
Could you elaborate?
Here's a good summary of the limited evidence for the benefits of strong type systems: https://danluu.com/empirical-pl/
Well Ruby kinda brought forth Crystal which while its own Programming Language is kinda Ruby but with Types.
> 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 get adding Scheme, but omitting CL seems like a big oversight
> > 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.
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.
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.
Here's a recent talk about how "concrete syntax matters, actually": https://www.youtube.com/watch?v=kQjrcSMYpaA
Highly recommended!
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?
The first should be a compile time error right, because `UInt8.ofNat` is going to require that its argument is 0-255. And the second should be a compile time error because subtraction should not give a `Nat` unless the first argument is definitely more than the second.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:
Kevin Buzzard even wrote a blog post about a similar question about division by zero: https://xenaproject.wordpress.com/2020/07/05/division-by-zer...> 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.
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.
>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.
> 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 `-_`.
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.
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.
Better than simply not encoding the actual invariants you care about.
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.
>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension,
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.
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.
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
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.
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
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"?
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
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.
It’s to show you’re too cool for grammar rules.
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.