|
|
|
|
|
|
by Taikonerd
56 days ago
|
|
|
> 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? |
|
|