Verifying Compiler is a system program that proves specified program properties besides translation of program. Paper represents overview of the research project that is entitled to design and implement a verifying compiler F@BOOL@, provides some theoretical background for feasibility of the project, discusses importance of verifying compilers for component-based approach to programming.
At the same time paper fixes formal syntax and operational semantics of a toy programming language Mini-NIL. This language is designed for approbation of basic concepts of the project and is a prototype of F@BOOL@ virtual machine. Publication is the first part of F@BOOL@ documentation.