The SPARK Formal project aims to develop a complete set of semantics of the SPARK language in Coq, for:
- - at the language level, ensuring the absence of ambiguity and the completeness of evaluation rules
- - at the tool level, ensuring the correct insertion of checks in the AST used for compilation and analysis
The formalization of SPARK also paves the way for the creation of proved toolchains for SPARK programs (a.k.a. “certified” toolchains in academia) such as CompCert.