Using agda2hs and ad-hoc Haskell FFI bindings, writing Qt applications in C++ with Agda- or Haskell-based backends (possibly including correctness proofs) is already possible. However, there was no repeatable methodology to do so, nor to use \emph{arbitrary} Haskell built-in libraries in Agda code. We present a well-documented, general methodology to address this, applying the ideas of the Model-View-ViewModel architecture to models implemented in functional languages. This is augmented by a software development kit providing easy installation and automated compilation. For obstacles arising, we provide solutions and ideas that are novel contributions by themselves. We describe and compare solutions for using arbitrary Haskell built-ins in Agda code, highlighting their advantages and disadvantages. Also, for user interruption, we present a new Haskell future design that, to the best of our knowledge, is the first to provide for arbitrary interruption and the first to provide for interruption via direct FFI calls from C and C++. Finally, we prove with benchmarks that the agda2hs compiler at the base of our methodology is viable when compared to other solutions, specifically to the OCaml extraction feature of Rocq and the default MAlonzo backend of Agda.

翻译：使用agda2hs和特定的Haskell FFI绑定，通过C++编写基于Agda或Haskell后端（可能包含正确性证明）的Qt应用程序已成为可能。然而，此前既缺乏可重复的方法论，也无法在Agda代码中使用任意Haskell内置库。我们提出了一种文档完善且通用的方法论来解决该问题，将模型-视图-视图模型架构的思想应用于以函数式语言实现的模型中，并通过提供简易安装与自动编译的软件开发工具包加以增强。针对过程中遇到的障碍，我们给出了本身具有创新贡献的解决方案与思路。我们描述并比较了在Agda代码中使用任意Haskell内置库的多种方案，突出其优缺点。此外，针对用户中断问题，我们提出了一种新的Haskell future设计——据我们所知，这是首个支持任意中断的方案，同时也是首个允许通过C和C++直接FFI调用实现中断的方案。最后，我们通过基准测试证明，与其他解决方案（尤其是Rocq的OCaml提取功能及Agda默认MAlonzo后端）相比，本方法论所依赖的agda2hs编译器具有可行性。