Abstract:
Low-level numerical libraries like GMP and BLAS are widely used. They are mostly written in C, Fortran, and Assembly, and make a heavy use of arrays and pointers. These languages are well-suited for writing efficient code but they are not safe, that is, they have many undefined behaviors, which increase the chance for bugs. Moreover, their semantics
make it difficult to reason about programs, and therefore to verify them; this is however a critical point because the correctness of numerical libraries is often subtle. Finally, the compilers for these languages are often very optimizing and thus very complex, which might reduce the confidence in the code they generate.

This work focuses on the design of a language, named Capla, and of its compiler. They address the aforementioned issues, while being well-suited to writing and verifying efficient low-level numerical libraries. In particular, the semantics of Capla, along with the proofs of type safety and of compiler correctness, have been formalized using the Rocq proof assistant.