Enhanced Agda-ChatGPT Integration for Iterative Type-Guided Code Synthesis

In this project, we developed a tool that combines the Agda compiler with the GPT API for an iterative, type-guided code synthesis process. Our method begins with GPT generating code snippets based on a given type and context from existing Agda code. When the Agda compiler encounters type errors, the error information is fed back to GPT, which then uses the feedback to generate an improved version of the code. This iterative process continues until the Agda type checker accepts the solution or a predetermined number of iterations is reached. Our main contribution is the development of a seamless integration between Agda and GPT that effectively utilizes Agda’s type system to guide AI-generated code. This approach aims to improve the reliability of AI-generated solutions and streamline the code refinement process.

Agda Backend for Elm Compiler: Bridging Formal Verification and Elm Web Applications

We have developed an Agda backend for the Elm compiler, which facilitates the direct translation of Elm web applications into Agda code. This enables developers to reason about Elm applications using Agda’s expressive type system, define desired behaviors, and prove that the Elm web application code adheres to the specified properties. Our work demonstrates the practical application of Agda as a verification tool for Elm web applications. This project highlights the potential of formal verification in ensuring safety and correctness for real-world software systems while extending Agda’s applicability to contemporary programming languages.

Deterministic Natural Language Translation of Agda Types: Fostering Accessibility and Communication

In this project, we have developed a tool that translates a subset of Agda types into natural language in a safe, predictable, and deterministic manner. This tool aims to make the specifications of web applications more accessible to developers who may not be well-versed in Agda’s formalisms. Our contribution focuses on improving communication between formal methods experts and average developers by bridging the gap between Agda’s formal type specifications and natural language descriptions. This work emphasizes the need for making formal methods more approachable, encouraging broader adoption and collaboration in the pursuit of safe and reliable software systems. In conclusion, our three subprojects work together to demonstrate a functioning system for the formal verification of Elm web applications. The key components of this pipeline are:

1. The Elm to Agda compiler, which translates Elm web application properties into Agda, providing a basis for formal reasoning using Agda’s type system.
2. The interactive integration between Agda and GPT, which automates the proof-generation process for desired properties through iterative refinement of code snippets based on Agda’s type errors.
3. The type translation tool, which offers insights by converting Agda types into natural language descriptions, making the formal verification process more accessible to developers.

Although our current work focuses on Elm web applications, a similar architecture could potentially be applied to various problems that can be formalized in Agda. It is important to note that the pipeline we have established is just the beginning, and further research and development will be required to fully realize its potential in the fields of AI-generated code and formal methods. By integrating these components into a cohesive pipeline, we aim to make modest progress toward improving the applicability of formal verification across a range of problems.