alt Hacker NewsYeah 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? :)
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? :)
Yes, 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.