The Agda SDK is a project intended to help developers utilising Agda-powered, provably correct backends in C++ Qt applications using the agda2hs compiler.
It consists of:
- installation scripts for fetching all the necessary tools from the Internet;
- a project template to get you started in no time;
- several pre-made frameworks to help you interact with the backend from C++ (e.g. Haskell futures);
- a documentation.
In order to utilise the SDK, a basic understanding of Agda and agda2hs is needed, as well as an intermediate proficiency in Haskell (i.e. knowing the IO monad and being able to navigate the documentation). However, frontend developers can join the C++ part of your project, even with no knowledge of Agda at all!
For more details, see the documentation. An example project is available under the even-counter branch.
And for even more details, see my paper on the SDK.