3 ms·
Lean has very little support for proving things about software. Right now, the community is mainly geared towards mathematics. This could change. Concrete Seman
by nextos 2y ago
Lean has very little support for proving things about software. Right now, the community is mainly geared towards mathematics. This could change. Concrete Semantics was rewritten in Lean [1], but I haven't seen more efforts geared towards software in the Lean community.
Dafny, Isabelle, Why3, Coq and F* have been used to verify non-trivial software artifacts. Liquid Haskell, Agda and others are also interesting, but less mature.
[1] https://browncs1951x.github.io/static/files/hitchhikersguide.pdf https://browncs1951x.github.io/static/files/hitchhikersguide...
- TypingOutBugs 2y agoAgda and Liquid Haskell are used for Cardano, one of the largest blockchain platforms, alongside other tooling in that space. It’s one of the larger formally verified projects in the wild so I’d argue it’s fairly mature. For example their formal specification of their ledger system: https://drops.dagstuhl.de/storage/01oasics/oasics-vol118-fmbc2024/OASIcs.FMBC.2024.2/OASIcs.FMBC.2024.2.pdf https://drops.dagstuhl.de/storage/01oasics/oasics-vol118-fmb...