Adapting the MVVM pattern to C++ frontends and Agda-based backends
This provides a structured methodology for developers building verified frontend applications with functional backends, though it appears incremental in adapting existing patterns.
The authors tackled the lack of a repeatable methodology for building Qt applications in C++ with Agda- or Haskell-based backends, presenting a general approach based on the Model-View-ViewModel architecture and a software development kit. They demonstrated viability with benchmarks showing the agda2hs compiler performs comparably to alternatives like Rocq's OCaml extraction and Agda's MAlonzo backend.
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.