Sorry, I only meant to address with some nuance the statement "A failure with logic should nuke due to the app being in an inconsistent state". If you are confident that the specific DFA code in the blog post will not fail, more power to you! And to us, which transitively trust the code via your judgment ;)

Edit. For technical geeking around:

* The point is about redundant check elimination, not full check elimination. A decent compiler should be able to eliminate redundant checks, though perhaps the language could offer some intrinsics (was: pragmas) to make this 100% reliable.

* For DFA proofs, perhaps something like https://courses.grainger.illinois.edu/cs373/fa2013/Lectures/... could be a start. A great intern may tackle it over a summer ;)