Posted by Jesper on November 11, 2020
I’m very glad and humbled to announce that I received an NWO Veni Grant for my proposal “A Trustworthy and Extensible Core Language for Agda.” You can read the official announcement on the NWO website. Thanks to this grant I will be able to focus on the development of Agda Core during the coming three years. Below, you can find the abstract of the proposal:
As software takes an increasingly central position in our society, being able to trust the software we use likewise becomes more and more important. Programming languages based on dependent types – such as Coq and Agda – provide a strong answer to this demand: they allow programmers to state the expected properties of a program, and the computer checks that these properties are satisfied before the program is ever executed. Yet the implementations of these languages are themselves just pieces of software, so can we really trust them? The problem is exacerbated by the multitude of extensions to these languages that make them more expressive and easier to use, but at the same time increase the number of components that must be trusted.
The goal of this project is to develop a fundamental approach to ensure the trustworthiness of dependently typed programming languages by means of a small core language that is deeply embedded into the full language. Embedding the core language within the full language erases the gap between its specification and implementation, minimizing the amount of code we have to trust and enabling us to do a meta-theoretic study to increase our trust even further. An embedded core language is also useful in practice: we intend to explore its potential as the basis for meta-programming and proof exchange with other languages. Concretely, we will develop Agda Core, a small and trustworthy core language for Agda embedded within Agda itself. In the development of Agda Core we will pay special attention to extensibility, providing a solid foundation for formalizing Agda’s various extensions. Thus we provide the basis for the next generation of programming languages that make it easy to develop programs that do what they are supposed to do, and nothing else.