alt Hacker NewsFor 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...
Replies
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.
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...
what about non-functional programming?
FP is just as irrelevant for most programmers as the math you already shoved aside
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.