Comment by kccqzy
20 hours ago
For the HN crowd who are generally programmers but not necessarily mathematicians, it’s more relevant to consider the programming side of things. There is a very good book (one I haven’t finished unfortunately) that covers Lean from a functional programming perspective rather than proving mathematics perspective: https://leanprover.github.io/functional_programming_in_lean/
I am learning Lean myself so forgive me as I have an overly rosy picture of it as a beginner. My current goal is to write and prove the kind of code normal programmers would write, such as real-world compression/decompression algorithms as in the recent lean-zip example: https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...
While reading though this book, I messed around with a basic computer algebra simplifier in Lean:
https://github.com/dharmatech/symbolism.lean
It's a port of code from C#.
Lean is astonishingly expressive.
Have you tried dafny, which seems roughly comparable for your purposes? I heard some buzz about it a little while ago but I haven't been following this space closely.
Dafny and F*, which competes directly with Lean but is more guided towards SWE, are definitely worthy of consideration.
Ada/SPARK may also be worth a look.
I recall an experiment in proving software correct from the 1990s that found more errors in the final proof annotations than in the software it had proved correct.
Then, I foresee 2 other obstacles, 1 of which may disappear:
1. Actually knowing what the software is supposed to do is hard. Understanding what the users actually want to do and what the customers are paying to do --which aren't necessarily the same thing--is complex
2. The quality of the work of many software developers is abysmal and I don't know why they would be better at a truth language than they are at Java or some other language.
Objection 2 may disappear to be replaced with AI systems with the attention to do what needs to be done. So perhaps things will change in that to make it worthwhile...
I think the hope for 2 is that those programmers would be forced into inaction by the language safety, rather than being allowed to cause problems.
I don't really think that works either, because there's endless ways to add complication even if you can't worsen behavior (assuming that's even possible). At best they might be caught eventually... but anyone who has worked in a large tech company knows at least a few people who are somehow still employed years later, despite constant ineptitude. Play The Game well enough and it's probably always possible.
It's even conceivable that 2 gets worse with AI: The AI does the proof for them, very convolutedly so, and as long as the proof checker eats it, it goes through. Comes the day when the complexity goes beyond what the AI assistant can handle and it gives up. At that point, the proof codes complexity will for a long time have passed the threshold of being comprehensible for any human and there is no progress possible. Hard stop.
2 replies →
Re 1: Discussing and guiding the desirable theorems for general-purpose programs has been a major challenge for us. Proofs for their own sake (bad?) vs glorious general results (good but hard?). Actual human guidance there can be critical there at least for now.
Mind linking the experiment? Sounds interesting.
Check out SeL4 (a proven correct micro kernel used by billions of devices worldwide) and CompCert (a proven correct C compiler used by Airbus).
what about non-functional programming?
FP is just as irrelevant for most programmers as the math you already shoved aside
Hmm like the “new” JS Fetch api with `then` chaining? What about map, filter, reduce? Anonymous functions? List comprehensions? FP is everywhere. Pure FP code isn’t seen very often, as side effects are necessary for most classes of programs, but neither is pure OOP code, as not everything is dynamically dispatched, nor imperative code, as Objects or functions may more cleanly describe/convey something in code.
I shoved math aside because I think for most of the HN crowd it wouldn’t be a good use of their time to do what mainstream mathematics is about, like the “things such as Grothendieck schemes and perfectoid spaces” the article also references. FP is much more relevant because for any program for which a proof of correctness is worthwhile, you can always extract a functional core of that program (functional core, imperative shell). And that functional core will be easier to prove than if it were written in an imperative style.
You might like looking at Dafny. It is more imperative focus, but has many of the same software proving functionality that Lean has.
It is different in that it uses SMT instead of dependent types and tactics to prove the software, but I found it more approachable.
Also, it compiles to several target languages, whereas Lean 4 only compiles to C and therefore only supports the C ABI.
FP and math are the same concept.
The semantics of math are equation based.
Everything in the math universal language is defined as an expression or formula.
All proofs are based on this concept.
To translate this into programming think about what programming is? Programming rather being a single line formula is a series of procedures.
in functional programming you get rid of that and you think from the perspective of how much of a program can you fit into a single one liner? An expression? Think map, reduce, list comprehensions, etc.
That is essentially what functional programming is. Fitting your entire program onto one line OR fitting it into a math expression.
The reason why you see multiple lines in FP languages is because of aliasing.
is really:
This is also isomorphic to the concept of immutability. By making things immutable your just aliasing part of the one liner...
So functional programming, one line programs, formulas and equations in math, and immutability are essentially ALL the same concept.
That is why lean is functional. Because it's math.