Our vision is to unlock the potential of humans and artificial intelligence (AI) alike by redefining the theory and practice of programming on the solid foundations of proof assistants. Proof assistants are computer tools that can automatically check the correctness of code against precise specifications. Such foundations will serve as the rails for the computer programming of tomorrow, enabling the rapid assembly of new theories and tools for digital systems.
Vision
Computing and code development underpin every aspect of our digital society and innovation, but producing software remains hard and expensive. With current methods, we can produce large amounts of very unreliable software or small amounts of very reliable one. With the acceleration of world-wide digitalisation, this is no longer an acceptable trade-off that we can build a future on.
The Centre for Formal Methods and Future Computing (FORM) aims to free us from this deadlock, by unlocking the large-scale application of formal methods: rigorous mathematical foundations for ensuring the reliability of computer systems.
At the core of FORM is the use of computer tools that can automatically vet mathematical developments and computer code. By using these tools, we envision a future where computer science knowledge can be accessed, advanced, and integrated as code, which computers can validate with mathematical certainty. These methods will be critical to unlocking the potential of artificial intelligence for computer programming: we will be able to use AI to help in the production of software and, at the same time, mathematical proofs that such software does what it is supposed to. Humans will be able to focus on specification – instructing what software is supposed to do – and formal methods will reliably check if specifications are respected. In this future, humans and AI can develop theory and practice of computing together, at speed, and with confidence.
CSlib: the Computer Science Library
FORM is the leading European centre on the development of the Computer Science Library (CSlib), the world’s first universal repository of computer science knowledge and tools. CSlib is the central instrument to realise the transformation we envision. It is an open source code repository written in Lean – a breakthrough technology that combines programming and mathematics, letting researchers write down mathematical theories and computer programs in a way that computers can automatically check for correctness.
CSlib is a global effort carried out in collaboration with world-leading stakeholders, and FORM is a key founding player in CSlib’s steering and technical leadership, together with Amazon, Google DeepMind, the Lean FRO (the Focused Research Organisation that steers the development of Lean), Stanford, and UT Austin.