Rendered at 01:29:12 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
thom 3 hours ago [-]
So this is all great, but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan? These seem like uniquely fragile software artifacts, despite the excellent and robust promises made by the runtime.
6gvONxR4sf7o 22 minutes ago [-]
Much of the point is that you have to understand the lean statement, not its proof. If the proof checker says it's good and reports that it just uses the usual axioms, then you can trust that they imply the statement. And the statement is never the 500k line part.
WalterGR 2 hours ago [-]
OP: Your article shows “[Contents]” where presumably the table of contents is to be displayed.
woggy 2 hours ago [-]
I’m curious whether people can use Lean primarily as a software specification language, without necessarily intending to prove everything.
Can we use it to specify module meanings and laws, to make the design precise and checkable, and would allow us to implement property based tests for those laws in our implementation. Lean becomes a tool for more precise thinking about the design.
keeganryan 1 hours ago [-]
Yes, absolutely. There's been a lot of work along these lines in other interactive theorem provers like Isabelle/HOL and Rocq. The general term to search is "Hoare logic," and I'm also a fan of the Concrete Semantics textbook. Lean is a very flexible language, but the main downside with Lean is that libraries for reasoning about program logic are comparatively less developed than Mathlib is for math.
fooker 3 hours ago [-]
Please do not try to understand Lean or proof assistants without first getting a rudimentary understanding of the logic involved. This article sort of skips over it, which is reasonable because it is pretty involved.
Even if you have written a large number of math proofs, you'd usually not have learnt the language or logic of proofs themselves. And even if you are an accomplished computer scientist, logic is not just AND, OR, NOT.
Here is some necessary reading, feel free to find better sources but wikipedia is good too.
Honestly, I'd say just play some of the lean games instead (https://adam.math.hhu.de/). I went through the dependent type theory and proof stuff first, and in hindsight it would have been much faster to just get the intuition first from learning to use a language like lean.
watt 4 hours ago [-]
This Lean stuff is gibberish and I don't understand why somebody thinks it's going to somehow make things better or simpler to understand.
vouaobrasil 34 minutes ago [-]
The thing is, it's not about making anything easier to understand. It's about padding academic CVs with something new.
fooker 3 hours ago [-]
Perhaps when you don't understand something, your first step should be trying to understand it?
Especially when it is something other smart people have been advocating.
Can we use it to specify module meanings and laws, to make the design precise and checkable, and would allow us to implement property based tests for those laws in our implementation. Lean becomes a tool for more precise thinking about the design.
Even if you have written a large number of math proofs, you'd usually not have learnt the language or logic of proofs themselves. And even if you are an accomplished computer scientist, logic is not just AND, OR, NOT.
Here is some necessary reading, feel free to find better sources but wikipedia is good too.
* Proof trees - https://en.wikipedia.org/wiki/Method_of_analytic_tableaux
* Constructive/Intuitionistic logic - https://en.wikipedia.org/wiki/Intuitionistic_logic
* Proofs and Types - https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
* (In)completeness - https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
* Compactness - https://en.wikipedia.org/wiki/Compactness_theorem
Especially when it is something other smart people have been advocating.