alt Hacker NewsI 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.
Replies
The @[grind] tactic has to be the single most important addition to Lean in terms of it's growing popularity
> I think the explosion in the popularity of Lean probably means that tactic-based proofs have won
The number of mentions of Lean in HN submissions aside, how do we gauge that? HN has odd trends like that - a decade ago, we loved everything "Bayesian" - but they don't necessarily translate to anything that's happening in the mainstream.
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)
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.
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!".