"Why not just use Lean?"
50 points by priime
50 points by priime
This is by Lawrence C Paulson, creator of Isabelle/HOL and very mildly shits on almost all other well known proof assistants for being the product of slightly insular communities with odd obsessions. It’s also very interesting and I will not attempt to summarize any of the substance.
Does anyone have a sort of succinct example or explainer of where Rocq's (as I understand it) constructivist approach "gets in the way"?
Is the idea here that if you don't need to construct the proof objects, then you can get law of excluded middle back and just create proofs out of thin air, whereas in Rocq you have to show up with the actual proof?
Something tells me this might be a part of the hint though:
The trick is to stop forcing everything to be a type.
I don’t have enough experience to answer your first question but on the second: I’m pretty sure you can just add the excluded middle as an axiom. Obviously a proof using that isn’t executable, but that’s not important if you’re not computing with your proofs.
But maybe this makes the whole user experience bad?
I don't have much personal experience, but I remember overhearing some discussion of the opposite direction having problems. A Rocq user wanting to do something constructive in Lean. (Partially remembered and without a deeper understanding to know if I'm misremembering)
The main user experience aspect is actually the ecosystem. Doing something constructively in Lean often means you can't use many parts of mathlib. Which makes sense in general but was aggravating in this instance because of the API choices: the proofs use Choice to derive some fact rather than externalising it.
i.e. a proof of a => b uses a non-constructive step that could have been (even trivially some times) constructive.
Or (and I'm going to get the formulation wrong) a proof of a => exists e => b where the e is then "choiced" out of thin air in the proof rather than being passed in as an argument. This means that you might have a concrete e at the call site but the proof doesn't let you thread it through. It forgets the witness in favour of just knowing that there is one.
I can imagine problems the other way too, even if you can have choice as an axiom, a lot of libraries are built constructively. It's less of a problem directly, but it means the structures used are more tailored towards constructive proofs. And there're less non-constructive libraries to build on.
This is a good overview of various benefits and downsides of dependent types with concrete examples: https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/26/slides/xavier.pdf.
They're slides from a talk given by Xavier Leroy, creator of OCaml and CompCert.
Putting on my typical tinfoil hat, but Microsoft being the owner or biggest funder of TypeScript, Rust, & Lean 4, I don’t like them having this much control of the languages ‘everyone’ is pushing. & yeah, there has been decades of languages in the proofs/theorem space with more maturity that everyone seems to be skipping on with the marketing push of Lean.
Both Rust and Lean are developed by non-profit foundations. Where the money comes from has a weight for sure but the development is open and I don’t see Microsoft people force-pushing things on Rust. For Lean we should talk about Amazon instead as said already in another comment.
I'm pretty sure that Amazon now has much more control over Lean, given that Leo de Moura (the creator of Lean) left Microsoft and is now employed by Amazon.
AFAIR, Amazon also employs Larry Paulson (author of this blog post & creator of Isabelle), so I guess you could make a similar point about them...
This wasn't mentioned in the post, but does anyone know where does Acron fit in that ecosystem in practice? (Or is it too early to talk about it yet?)
While I'm not really into the theoretical maths, their (as I understand it) "just keep on building a massive repository of fragments" approach is fascinating.