Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

The author of Z3, Leo de Moura, released Lean 4 milestone 1 about 3 weeks ago: https://github.com/leanprover/lean4

Lean 4 is a functional programming language and theorem prover that compiles to C. A lot of research went into making Lean 4 blazingly fast https://leanprover.github.io/publications/

Galois inc reproduced benchmarks by the Lean 4 devs that show that Lean 4 regularly outperforms the C++ stdlib.

This is an awesome mix of raw speed, functional programming, and formal software verification.



but how is Lean related to Z3? model checking and dependently typed programming are totally orthogonal, right?


I don't know about that. You can obviously use them for similar things. Namely, proving properties about your software.

Here's a good blog post talking about type theory vs logics: https://ucsd-progsys.github.io/liquidhaskell-blog/2019/10/20...




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: