His solution and syntax remind me of Ada's variant records. Despite Ada's focus on safety, it also resorts to runtime exceptions for incompatible fields in that case. That's probably a local maximum in the language design space.
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.
