WUFFS is provably safe - that's the whole schtick. If a WUFFS kernel exists, you can assume it is safe. If it's not proven safe, it doesn't compile. The reason everyone doesn't program in WUFFS is that you have to write a proof that your kernel is safe, which takes a very very very long time.
For WUFFS the language, or for WUFFS the library, or for the WUFFS tooling today?
The clever idea is to have you the programmer in effect write a proof that your code has the desired semantic properties as part of the programming activity and so then the WUFFS transpiler is merely checking that the proof is correct.
This leverages your understanding of what you were trying to do.
If you point out some of the above has run-state in some situations... it is provably nondeterministic... and thus the assertion of correctness is utter nonsense.
Hardly a panacea for fundamentally bad designs that go back decades.
Ever seen a web-server written in postscript? Its worth a look just for the laughs.
