Absicht und so wird später hinzugefügt.

Ein bisschen eine Antwort auf die folgende Frage, die auf lobste.rs gestellt wurde: lobste.rs : What software do you dream about, but do not have time to do yourself?

Der grösstmögliche Rahmen

  1. Formale Spezifikation einer ISA.
  2. Formale Spezifikation einer Programmiersprache.
  3. Ein Compiler von dieser Programmiersprache zu dieser ISA. Mit formalem „Korrektheitsbeweis“.
  4. Programme in dieser Programmiersprache, von welchen man mit Punkt 2 die „Korrektheitseigenschaften“ bewiesen hat.
  5. Eine (bewiesen korrekte) Implementation der ISA um darauf die Programme laufen zu lassen.

Das ist die grundsätzliche Struktur. Bei jedem Punkt gibt es Entscheidungen mit denen man das „Gesamtprojekt“ mehr oder weniger kompliziert machen kann. Zum Beispiel: je „unähnlicher“ die Programmiersprache (Punkt 2) der ISA (Punkt 1) ist, desto komplizierter wird der Compiler (Punkt 3). Ausserdem könnte man den Compiler wie LLVM konstruieren, um die Struktur des Compilers zu vereinfachen und um ihn vom ISA unabhängiger zu machen. So könnte man verschiedene ISA für Punkt 1 wählen und verschiedene Sprachen für Punkt 2.

Die Projektskizze von Amal Ahmed in „Verified Compilers for a Multi-Language World“ geht in diese Richtung, betrifft aber „nur“ Punkte 2 & 3. GNU Guix mit seinen reproduzierbaren Paketen würde bei der Verwaltung von Programmen (Punkt 4) sicher helfen.

Beweisassistent

Für ein solches Projekt wäre ein guter Beweisassistent, bzw. eine gute Zusammenarbeit zwischen Beweisassistenten nötig. Vlt. liefert https://kwarc.info geeignete Werkzeuge und Ideen. (Insbesondere das “QED Reloaded” Paper und seine Bibliographie)