Um einen Übersetzer für eine höhere Programmiersprache PL auf einer
Zielmaschine TM zu implementieren, empfiehlt sich das Bootstrapping
mit vorhandenem unverifizierten Übersetzer für eine Obersprache PL0
auf einem Wirtprozessor HM0. Wegen dieses Univerifiziertseins sollte
man den sog. starken Übersetzertest durchführen. Durch Einschleusen
von Viren kann der Test aber von einem versierten Hacker überlistet
werden.  Ein Implementierungskorrektheitsbeweis hätte die Viren
aufgedeckt. Im Sinne der Theorie der Testdatenselektion von
J.B. Goodenough und S.L. Gerhart genügt aber ein eingeschränkter
Beweis, um trotzdem volle Übersetzerkorrektheit zu garantieren.