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

▲

dharmatech 43 minutes ago | parent | next [-]

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.

▲

readthenotes1 3 hours ago | parent | prev | next [-]

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

▲

Groxx an hour ago | parent | next [-]

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.

▲

jsmorph 3 hours ago | parent | prev | next [-]

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.

▲

cayley_graph 3 hours ago | parent | prev [-]

Mind linking the experiment? Sounds interesting.

	▲	3 hours ago \| parent [-]
		[deleted]

▲

NooneAtAll3 33 minutes ago | parent | prev [-]

what about non-functional programming?

FP is just as irrelevant for most programmers as the math you already shoved aside

	▲	DauntingPear7 13 minutes ago \| parent [-]
		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.