Mission: improve the software and hardware development process by replacing ugly development techniques with beautiful ones
Secret weapon: applied mathematical logic, including computer theorem proving (especially Coq) and type systems
Our basic mission is to build the programming platform of the future, based on close integration of computer theorem-proving tools, especially the Coq proof assistant.
While formal methods are commonly viewed today as an extra (and non-cost-effective!) activity piled on top of the normal programming process, we believe that machine-checked proofs will have a transformative effect on the development process by enabling new forms of abstraction and modularity, with associated benefits in lowered human effort and improved security and performance.
We are gradually piecing together a proof-of-concept platform that runs inside of Coq, where the theorem prover becomes the IDE that the programmer interacts with primarily from the beginning of a project.
Ongoing work considers different abstraction levels, including mathematical specifications, functional programs, imperative programs, assembly language, and circuits suitable to be turned into hardware. A running theme throughout the different layers is highly automated formal proofs that still prove deep theorems from first principles. We also use functional programming with rich type systems almost everywhere.
