> The signature declares types, preconditions, postconditions, and effects. The compiler verifies the contract via SMT solver.
This reminds me of Dafny: https://dafny.org/
Actually, that's an interesting question: how good are LLMs at writing Dafny?
This reminds me of Dafny: https://dafny.org/
Actually, that's an interesting question: how good are LLMs at writing Dafny?
No comments yet.