๐ TypeScript verification
Our goal is to bring formal verificationย ๐ก๏ธ to TypeScript in the same way TypeScript brings typing to JavaScript.
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-js to translate JavaScript code to Coq using the Babel parser. You can try it with our ๐ฝ๏ธย demoย where you type JavaScript code on the left and see the Coq translation on the right. This works on untyped JavaScript. However it seems some type information would be helpful for the translation, so we are now directly targeting the translation of TypeScript (instead of untyped JavaScript).
- coq-of-ts to translate TypeScript code to Coq, using the TypeScript compiler API. This follows the
coq-of-js
project and is under development.
Offer
For any additional information or service request, if you have code to verify or to develop, contact us:
- by email at contact@formal.landย โ๏ธ
- with a call on koalendar.com/e/meet-with-formal-landย โ๏ธ
Helping you buildย ๐