In jedem größeren Softwareprojekt stellt sich früher oder später die Frage, ob unentdeckte Fehler im Code schlummern und den korrekten Ablauf des eigentlich gewünschten Prozesses in bestimmten Situationen sabotieren. Unter dem Wikipedia-Stichwort Programmfehler findet man hierzu die Aussage, dass als stabil geltende Programme durchaus eine Fehlerdichte von bis zu einem Fehler je 2000 Programmzeilen aufweisen können.
Welche Bedeutung dem Thema zukommt, wird klar, wenn man an die Unfallgefahren in sicherheitskritischen Bereichen und auch die immensen wirtschaftlichen Schäden denkt, die durch Programmfehler entstehen. In der Informatik wird daher über Fehlererkennung und -vermeidung intensiv geforscht und ein großes Sortiment an Lösungsansätzen steht bereits zur Verfügung, wobei man in der Praxis nur eine Verringerung der Fehlerhäufigkeit und keinen hundertprozentigen Schutz erwarten kann. Das liegt auch daran, dass die Fehlerdetektion eine Definition des korrekten Prozessablaufs für alle möglichen Eingabedaten benötigt und diese in vielen Fällen gar nicht präzise vorliegt.
Einen gewissen Sonderfall spielen in dieser Hinsicht Programme der numerischen Mathematik, mit denen Darstellungen von mathematischen Objekten (Zahlen, Mengen, Funktionen, ...) berechnet werden sollen. Da hier sowohl das Ziel als auch der Algorithmus präzise in mathematischer Sprache formulierbar sind, ist die Fehlerfreiheit prinzipiell mit mathematischer Strenge beweisbar. Bei maschineller Prüfung dieses Korrektheitsbeweises und anschließender automatischer Übersetzung des Algorithmus in die gewünschte Programmiersprache, entsteht Programmcode, der frei von syntaktischen und logischen Fehlern ist.
Im Projekt $\mmath$ werden genau solche Compiler entwickelt, wobei sich die zugrunde liegende formale Sprache sehr eng an übliche mathematische Notationen anlehnt. Ausgehend von Grundalgorithmen, deren Korrektheit angenommen wird (analog zu den Axiomen einer Theorie), können dann immer komplexere Algorithmen mit beweisbaren Eigenschaften konstruiert werden.
Eine Absicherung nach unten erhält man ganz im Sinne des axiomatischen Ansatzes von Hilbert dadurch, dass auch die Grundalgorithmen sukkzessive auf immer weniger und möglichst elementare Basisalgorithmen zurückgeführt werden können (Axiomatisches Denken, David Hilbert, Mathematische Annalen, Vol. 78, pp. 405-415, Springer, 1917).
