Bridging gaps in numerical math

When it comes to the implementation of a carefully derived and theoretically well founded numerical algorithm, the formal setting of mathematics is generally left. As a result the programs are prone to logical errors caused by typos and technical details dictated by the programming language or by efficiency reasons. To find these errors, programs can usually only be tested with some examplary cases leading to exercises of the form "Implement the algorithm and show its correctness by running some examples". In other parts of mathematics such exercises would be highly uncommon!

This leads to the question whether parts of the implementation process can be integrated into the mathematical formalism to reduce their error rate. A natural answer to this question again emphasizes the role of modeling: If one models the relevant aspects of the programming language and derives and verifies the algorithms mathematically within this model, the resulting representation can lead to implementations free of both syntactic and logical errors if tools are available which turn it into code automatically. Then, only the modeling error remains (e.g. that computer reals are modeled by mathematical real numbers) which may be reduced, as usual, by employing more sophisticated models.

In order to support this approach, a long term goal of the $\mmath$-project is to provide methods to formulate logically verified algorithms as models in the $\mmath$-language and a code generator that creates code from those models for different programming languages.

As a preliminary step, a Scala library is developed providing classes that represent common mathematical concepts and their functionality (like polynomials, matrices, vector spaces,...). It allows to implement numerical algorithms with the same objects that were used in their derivation which removes the error-prone transformation of mathematical objects into language specific representations.