🌐 TypeScript verification
Formal verification is a strong method to ensure that code does not contain bugs or security issues 🧨 and improve the QA process. This is thanks to the use of mathematical methods 📐. With formal verification, we can probably hope to divide by one hundred the number of bugs on a code that is already well-typed and tested. If the verification is cost-effective enough, we can apply it on a large class of programs to improve the quality of existing software 🌟.
Our strategy is to consider a convenient subset of TypeScript (essentially a purely functional subset) and make an automatic translation to similar-looking Coq code. The Coq 🐓 system is an interactive proof assistant that allows to verify arbitrary specifications on programs, either automatically or with manual guidance. Our translation to Coq might or might not be 100% faithful. The goal is to be efficient even if we need some approximations.
We have two projects:
- coq-of-ts to translate TypeScript code to Coq, using the TypeScript compiler API. This follows the
coq-of-jsproject and is under development.
Helping you build 🚀