Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.




Consider applying for YC's Summer 2026 batch! Applications are open till May 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: