I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you run it interactively and observe the goals at each step. In contrast languages like Idris do not use tactics and require explicit manipulation of proof objects; it’s a lot less automated and verbose. Using the function call analogy, it’s like having to write down every argument passed to a function call and name every return value. It’s more tedious to write but both the writer and the reader gain more by the explicitness. But in the age of AI, the tedium to write proofs without tactics really shouldn’t have mattered.
Introduction to Formal Verification with Lean Part 1
21–30 of 55 posts
Re: Introduction to Formal Verification with Lean Part 1
#22how is lean different from tlaplus for helping you with reasoning during the design phase?
I literally just discovered tlaplus last week after struggling with reasoning about the explosion of permutations about configuration policies Im designing, and Im still learning the math but Im finding it easier to reason with tlaplus than in code is lean like that?
Re: Introduction to Formal Verification with Lean Part 1
#23If you like Lean, here are two more great, short books on proving things about your program (not with Lean, though):
1. https://mitpress.mit.edu/9780262527958/the-little-prover/
2. https://mitpress.mit.edu/9780262536431/the-little-typer/
David Thrane Christiansen, co-author of the second, also wrote Functional Programming in Lean (Lean 4) among many other tutorials and things.
Re: Introduction to Formal Verification with Lean Part 1
#24I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you…
I'll note that not all segments of a proof are equally interesting. Many steps, perhaps even most when it comes to proofs about programs, are "obvious". I find that tactic-based proofs tend to be more legible than providing very explicit proof objects directly, because it allows the obvious but tedious details to be elided. What you are left with are just the most important high-level steps that the automation couldn't infer (or which we just don't wish to delegate). Things like "induct according to this scheme after generalizing this variable" or "first prove this auxiliary lemma" or "apply this inverse function to both sides so that they cancel".
I'd also argue that automation is essential to practical proof engineering. It make the proofs less brittle to minor changes and therefore more maintainable.
Edit: a couple more thoughts. First, there is nothing stopping you from defining proof objects directly in Lean without tactics. That flexibility is quite nice -- you can automate as much or as little as you like. Of course, in practice, people almost always use tactics. Second, I use the ACL2 prover quite a bit, which is not tactic-based. Instead, you give high-level "hints" that steer the aggressively-automated prover. Funny enough, I have colleagues that look at Lean proofs and say "these proofs are so verbose, how does anyone understand them!".
Re: Introduction to Formal Verification with Lean Part 1
#25I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you…
I don't really buy this argument because we can all read the code with the Lean LSP.
Also, after using a tactic enough you can guess why it's used.
Agda and Idris are more beautiful for sure, but a proof is a proof (according to the law of the excluded middle)
Re: Introduction to Formal Verification with Lean Part 1
#26how is lean different from tlaplus for helping you with reasoning during the design phase? I literally just discovered tlaplus last week after struggling with reasoning about the explosion of permutations about configuration policies Im designing, and Im still learning the math but Im finding it easier to reason with tlaplus than in code is lean like that?
You can embed TLA+ into Lean. I don't think that there's any benefit to formalization before coding unless you're working on like million dollar projects
Re: Introduction to Formal Verification with Lean Part 1
#27The Natural Numbers Game is amazing, highly recommended.
> In this game you recreate the natural numbers N from the Peano axioms, learning the basics about theorem proving in Lean.
Re: Introduction to Formal Verification with Lean Part 1
#28Why does Lean always have a way to mess up your file system, writing to any files, rather than just proving proofs?
I found that out when reading the recent articls about counterexamples.
Re: Introduction to Formal Verification with Lean Part 1
#29(Asking as an interested noob) -- How is this different to something like 'assert' statements in Python?
Assertions are for testing at runtime. They demonstrate that the behavior is correct on one input when it runs. Formal verification proves that the code is correct on _all_ inputs _before_ it runs.
Formal verification proves if your specified theorem is correct. You can state any number of properties, in one extreme you just have basic types.
The interesting, 'hard-to-wrap one's head around' thing is that this verification is done by basically comparing arbitrary computations for equality.
So to prove that `3+3 == 6`, you would create an object with the type being `3+3 == 6`. And the rules of these languages are such, that the only way you can ever create an instance and thus a valid object for this type is if it's a true statement. 3+3==7 has no instance and can never have. (Interestingly, the instance of the above type is called `refl` for reflexivity. This is the only instance possible, and its type is basically a generic expecting a type, and a value of that type (this is where dependent types come in). Its "constructor" will place a single value into both slots, so the only way it can ever be instantiated is via values that the language/compiler itself considers equal.
A proof is just a manipulation of each "side" until they are trivially equal to each other).
One important caveat of the above: these languages evaluate expression not like most ordinary languages, like stopping at a thunk when the outermost value can't be further simplified. They will continue inward simplifying everything, and comparing these together - so even functions can be compared (though implementation matters a lot, and will alter the shape of proofs!)
Re: Introduction to Formal Verification with Lean Part 1
#30I think the explosion in the popularity of Lean probably means that tactic-based proofs have won. I wrote many proofs in college and on mere aesthetic grounds I avoided the use of theorem provers with tactics. Invoking a tactic is like calling a function without writing down what the arguments to the function are and what the result of the function is. As a reader you gain little knowledge about the proof unless you…
Lean's mostly used for maths, and tactics are much more ergonomic there. For writing correct-by-construction software programs, complex dependently-typed objects can be more ergonomic, as they allow passing a bunch of invariants through a program that are correct by construction, rather than needing to prove them at every stage via tactics.