A correct-by-construction approach to approximate computation

Correct-by-construction program development uses advanced type systems to describe both the data manipulated by computation, and the correctness of those computations. Embedding correctness within software has many advantages, as certified by several decades of pioneering work in the UK and elsewhere, which have culminated in systems such as Agda, Idris, Coq, Lean, HOL, Isabelle, etc., which are powerful enough to implement this vision and which are now having significant impact in both academia and industry.

The main question that motivates this research is: can correct-by-construction programming be extended to computation with approximate values, e.g. in: i) stochastic systems where one needs to handle inherent/simulated randomness; ii) resource limited environments, where exact computation is prohibitively expensive; iii) systems with imperfect/partial recall, where one only has limited information about what has happened or the intentions/trustworthiness of each agent; and iv) non-exact computation where primitive data (e.g. from sensors) is inexact and supplied with error bars. These scenarios arise in e.g. cyber-physical systems, machine learning, robotics, automotive engineering, aerospace, and energy systems. Measuring how close measurements might be from their true values naturally leads to the use of metrics but, despite some successes, their use suffers from a number of drawbacks, e.g. i) metrics defined in one problem domain often do not carry over to others; ii) metrics based upon system structure often do not reflect behavioural similarity and vice-versa; and iii) increasingly accurate models of a system's structure are not guaranteed to have increasingly accurate behaviours to that of the modelled system.
We conjecture that these problems are manifestations of the deeper problem that all of the mathematics underpinning computation takes exact equality as primitive, so approximation is built over an exact meta-theory. However, in a recent...