| ▲ | c0balt 2 hours ago | |
Isabelle/HOL as a language is nice, but the tooling has deep flaws even outside the pure desktop-first app approach. The language is different (not necessarily better) in comparison to Lean, but I do agree with some of the points on dependent types. It seems both languages mostly just made different tradeoffs, which imo, were fair and have shaped them into quite efficient tools for their domains. The domain of "proofs" is large and different paradigms just have different strengths/weaknesses, Lean just specialized for a different part of this space. Sledgehammer is nice but probably just a question of time until an equivalent can be ported/created for Lean. It might also be nice to use for explorative phases but is a resource hog, it also makes proofs concise but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer". Working on Isabelle itself however is painful (especially communicating with developers) in comparison to Lean. Things like "we don't have bugs just unexpected behaviour" on the mailing list just seems childish/unprofessional. The callout to RAM consumption of Lean and related systems is also a bit of joke when looking at Isabelle's gluttony for RAM. | ||
| ▲ | zozbot234 2 hours ago | parent | next [-] | |
> but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer". One issue with this is that coming up with a quickly-checkable certificate for UNSAT is not exactly a trivial problem. It's effectively the same as writing a formal proof. | ||
| ▲ | vintermann 2 hours ago | parent | prev | next [-] | |
Last I checked, Isabelle/HOL used a custom Emacs mode as their interface. (I could be mixing it up with one of the other HOLs). | ||
| ▲ | thaumasiotes 36 minutes ago | parent | prev [-] | |
> Sledgehammer is nice but probably just a question of time until an equivalent can be ported/created for Lean. I have no knowledge of what sledgehammer is. However... > it also makes proofs concise but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer" This description makes sledgehammer sound identical to Mathlib's `grind`. https://leanprover-community.github.io/mathlib4_docs/Init/Gr... | ||