A Perfectable Programming Language

spankalee

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.

ilsubyeega

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

zem

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

travisgriggs

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

solomonb

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.

whacked_new

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

heliumtera

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

unexpectedtrap

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.

xarope

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.

psychoslave

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.

dharmatech

I've been messing around with a computer algebra simplifier in Lean: https://github.com/dharmatech/symbolism.lean Lean is astonishingly expressive.

snthpy

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.