A Perfectable Programming Language
alok.github.io68 points by yuppiemephisto 6 hours ago
68 points by yuppiemephisto 6 hours ago
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.
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.
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 ..."
i like this website, it shows documentation when hovering the code while i see similar stuffs really rare in web blog areas
wait, I'm intrigued, it says the blog itself is lean code. How? It's rendered, like pollen?
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
>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension,
Lol
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.
Is it due to the feature that the author claimed "this blog post is itself Lean code"?
its not caused by a habit of writing authentically formatted Homestuck rp smut
but surely its correlated
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.