@pervognsen @tmyklebu This Dafny Workshop talk on industrial coding style is pretty telling:
https://www.youtube.com/watch?v=IicF7UYZ4UY
It seems that automatic management of the context quickly gets out of hand in a large project, and you need to shift to a style of using opaque functions, API lemmas, etc. They even abandon the use of postconditions!
=> More informations about this toot | View the thread | More toots from zwarich@hachyderm.io
=> View pervognsen@mastodon.social profile | View tmyklebu@mastodon.gamedev.place profile
text/geminiThis content has been proxied by September (ba2dc).