[HymnOfCreation]

Ada offers formal verification to remove checks, they can also be removed without formal verification but that is not a sane thing to do. Ada feels like it is more about writing the correct intent of programmers and caring more about intent than any other thing. For example, the pre and postconditions are not always meant to be 100% verifiable, its fine for them to not be verifiable, the checks are more important than the verifiablility of them.