2 ms·

Whether you should trust the compiler is always an issue. The answer is no.

• Animats 10y ago
  True. It's also easier to let the regular compiler front end do a lot of the work. Verification can occur after templates have been instantiated, macros have run, types have been determined, structure field offsets have been assigned, and syntax errors have been detected. This gets rid of most ambiguities of working at the source code level. In the early days of program verification it was popular to work at the source code level, because automatic efforts were trying to emulate what humans were doing by hand. Early programming verification was trying to emulate what mathematicians did. Efforts were made to describe languages axiomatically at the source level. Now that's recognized as both very hard and likely to lead to errors.