> The signature declares types, preconditions, postconditions, and effects. The compiler verifies the contract via SMT solver. This reminds me of Dafny: https:

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