Die Struktur des initialen, korrekt und korrekt implementierten
Übersetzers paßt sich in die Architektur zur Konstruktion korrekter
Übersetzer ein. Die Übersetzung ist in 4 Schritte eingeteilt; 3
Zwischensprachen SIL, Cint und TASM sind dazu definiert
worden. Ausgehend von korrekten Übersetzungsspezifikationen werden
Übersetzerprogramme in der Quellsprache, hier ComLisp, selbst korrekt
konstruiert. Durch einen Bootstrap mit anschließendem Beweis durch
Probe kann die korrekte Implementierung des Übersetzers auch im
Maschinencode, hier dem des Transputers, bewiesen werden.