Comment by bneb-dev

4 days ago

Salt chose Z3 because it felt right for a compiler. The 100ms timeout means it's not sound, but it's useful. Lean could be the right choice when a proof is a hard requirement?

0 comments