alt.hn

4/12/2026 at 9:11:24 PM

A perfectable programming language

 https://alok.github.io/lean-pages/perfectable-lean/

by yuppiemephisto

4/13/2026 at 7:51:41 AM

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

by kleiba2

4/13/2026 at 2:40:16 AM

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.

by unexpectedtrap

4/13/2026 at 9:42:48 AM

Static linking wonders?

Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.

by pjmlp

4/13/2026 at 4:18:47 AM

Lean is far off the most bloated one. Isabelle most likely takes that spot, the main archive includes a whole vscodium among other things.

by c0balt

4/13/2026 at 8:58:32 AM

>> 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 :)

by senko

4/13/2026 at 2:00:45 AM

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.

by solomonb

4/13/2026 at 1:54:46 AM

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

by travisgriggs

4/13/2026 at 6:32:25 AM

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

by riffraff

4/13/2026 at 9:02:05 AM

XL is a very interesting modern iteration on extensible languages, unfortunately it seems abandoned.

by mapcars

4/13/2026 at 4:01:01 AM

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.

by psychoslave

4/13/2026 at 4:16:36 AM

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)

by c0balt

4/13/2026 at 10:37:00 AM

A very polite reminder that Elixir exists.

by neya

4/12/2026 at 11:22:47 PM

i like this website, it shows documentation when hovering the code while i see similar stuffs really rare in web blog areas

by ilsubyeega

4/13/2026 at 5:54:38 AM

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.

by snthpy

4/13/2026 at 9:26:00 AM

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

by andai

4/13/2026 at 3:33:14 AM

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.

by xarope

4/13/2026 at 6:29:00 AM

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

by shevy-java

4/13/2026 at 10:45:05 AM

> do not acknowledge trade-offs when it comes to type systems

Could you elaborate?

by vouwfietsman

4/13/2026 at 6:32:08 AM

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

by ChadNauseam

4/13/2026 at 7:23:54 AM

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

by andersmurphy

4/13/2026 at 6:57:35 AM

Well Ruby kinda brought forth Crystal which while its own Programming Language is kinda Ruby but with Types.

by mastermage

4/13/2026 at 2:11:19 AM

wait, I'm intrigued, it says the blog itself is lean code. How? It's rendered, like pollen?

by whacked_new

4/13/2026 at 3:59:44 AM

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

by ajs1998

4/13/2026 at 7:39:58 AM

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?

  #eval (UInt8.ofNat 256 : UInt8)
  #eval (4 - 5 : Nat)
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.

by IshKebab

4/13/2026 at 10:17:19 AM

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.

by JuniperMesos

4/13/2026 at 8:39:48 AM

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:

  def x := #[1, 2, 3, 4]
  #check x[7]
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...

by unexpectedtrap

4/13/2026 at 2:12:42 AM

>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension,

Lol

by heliumtera

4/13/2026 at 3:16:51 AM

It makes complete sense to polish that usecase.

by adamnemecek

4/12/2026 at 11:02:27 PM

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.

by spankalee

4/12/2026 at 11:58:47 PM

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.

by losvedir

4/13/2026 at 4:15:35 AM

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

by noosphr

4/12/2026 at 11:35:30 PM

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.

by JuniperMesos

4/13/2026 at 2:12:41 AM

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.

by bobanrocky

4/13/2026 at 2:29:17 AM

I ReSpEcTfUlLy DiSaGrEe FrIeNd -- PeOpLe LoVe SlOp. =3

by Joel_Mckay

4/13/2026 at 5:52:43 AM

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.

by ajkjk

4/13/2026 at 2:05:36 AM

its not caused by a habit of writing authentically formatted Homestuck rp smut

but surely its correlated

by QuadmasterXLII

4/13/2026 at 2:28:02 AM

Is it due to the feature that the author claimed "this blog post is itself Lean code"?

by jason1cho

4/13/2026 at 4:20:41 AM

It’s to show you’re too cool for grammar rules.

by GeoPolAlt

4/13/2026 at 1:12:42 AM

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

by trueno

4/13/2026 at 2:37:30 AM

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.

by binary132

4/13/2026 at 1:07:04 AM

The swearing is another thing I keep seeing more of.

by giancarlostoro

4/13/2026 at 6:36:34 AM

clojure exists as an example of people trying types and then realising it's cruft and not needed.

by danieltanfh95