A Perfectable Programming Language

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.

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 messing around with a computer algebra simplifier in Lean:

https://github.com/dharmatech/symbolism.lean

Lean is astonishingly expressive.

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

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 like this website, it shows documentation when hovering the code while i see similar stuffs really rare in web blog areas

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.

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

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

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