[nigeltao]

That's how WUFFS (Wrangling Untrusted File Formats Safely) works:

https://github.com/google/wuffs#what-does-compile-time-check...

[LoganDark]

WUFFS is awesome. It won't even let you add two ints without proving they cannot overflow