3 ms·
but how is Lean related to Z3? model checking and dependently typed programming are totally orthogonal, right?
by iso8859-1 6y ago
but how is Lean related to Z3? model checking and dependently typed programming are totally orthogonal, right?
- the-smug-one 6y agoI 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/why-types.lhs/ https://ucsd-progsys.github.io/liquidhaskell-blog/2019/10/20...