Many programming languages have a distinct compilation phase and a run-time phase. I propose introducing a new separate phase for static verification.

Programmers want to verify a lot of different properties of their code at compile-time. Some examples are:

• assuring that type-casts are valid 
• assuring visibility rules are respected
• assuring that "constness" or mutability guarantees are maintained
• assuring that overrides are provided for virtual functions
• assuring that virtual function hiding is not done implicitly (e.g. in C# using "new" or "virtual")
• assuring that variables are initialized before used

There are ideas and proposals to check even more things at compile-time in various languages. Some of the examples are:

•  assuring that class invariants are valid (where it is possible to prove so)
• checking preconditions and postconditions are legal
• checking that certain parameters are never null
• running unit-tests
• checking that utility and non-utility functions, are valid.

Many of these tasks are verifications that can be performed at run-time in a language that supports introspection or reflection. The problem with adding introspection is that it somewhat inhibits the compiler's ability to optimize code: it has to maintain a complete representation of the code just for examination.  The other problem is that this verification doesn't need to be done at run-time, it only needs to be done by the developer, so there is an undue performance hit if we run all of the code during every execution. One solution is to turn on and off the verification part of the code using pragmas or macros, but the compiler has no sense whether we want to generate the abstract representation of the code.

I propose that instead of implicitly performing many of these checks that a language should provide the facilities (introspection) and libraries (such as a theorem prover) for verifying the various properties of code. This would be done in a separate verification phase that occurs immediately after compilation. The verification phase would be like running a separate program woven into your main program, which has complete read-only access to the abstract syntax tree.

What do you think of this idea? Would you like to have better control over verifying the static properties of your code? Do you think it would encourage better programming practices such as unit-testing, and usage of programming contracts? What could you do with this kind of reflection in a language like C++, that you can't do now?