3 ms·
Yeah I can see pointer weirdness being an issue. As for being not expressive enough for specifications, isn't the code itself a form of specification? :)
by fooker 11mo ago
Yeah I can see pointer weirdness being an issue.
As for being not expressive enough for specifications, isn't the code itself a form of specification? :)
- cake-rusk 11mo agoYes, but the quality of the spec varies. For example many (most?) C programs have undefined behaviors which means the spec is incomplete and unreliable. Dafny gives you better tools to avoid this. So in the end you get a higher quality spec with Dafny.