Hacker News Reader

Comment by thunkingdeep | Hacker News Reader

In what situations would one prefer this vs Lean?

This seems to compile to native code if desired, so does that mean it’s faster than Lean?

Forgive me if these are obvious questions, I’m just curious and on my phone right now away from my machine.

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...

Agda 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-fmb...

One technical difference is that F* heavily uses SMT automation, which is less emphasized in Lean (their book even says that F* typechecking is undecidable). F* programmers frequently talk about the language's emphasis on monadic programming, which I'll admit that I don't understand (but would like to!)

As long as you understand that a monad is a monad, you should be fine!

Looking at publications on the home pages for both projects it seems F* results in more practical stuff like hardened cryptography and memory allocation libraries, while Lean presents itself as more of an experiment in developing proof assistants.

> F* is oriented toward verified, effectful functional programming for real-world software, while Lean is geared toward interactive theorem proving and formalizing mathematical theories, though both support dependent types and can serve as general-purpose functional languages in principle.

Lean also started at MSR, and nowadays is bootstraped, they use different approaches.

Reply on news.ycombinator.com