I cant remember Thompson's stuff: Im talking the general problem. You're correct in that my first step shifts the problem: does it on purpose. Here's what subversion resistant development takes: modular software with sensible interfaces: ability to understand code for human review (closer to algorithm the better); ability to understand compiler passes in isolation; ability to implement toolchain in language of choosing. There are existing flows like this as I illustrated. So, you use them and leverage diverse audience to check results. I mean, would you rather implement CompCert passes by hand or GCC even without optimizations? See the difference? ;)
Now, I did have a method to solve problem you're addressing. You implement an assembler first. Then a macro assembler with macro's for HLL primitives. You can use that immediately to jmplement certified compiler. Alternately, you can pick up Oberon report or Scheme book to implement that to get a true HLL plus compiler. Then you implememt the certified compiler with it. Comprehension, code complexity, and trust are kept manageable by building layer by layer. This, for productivity not security, is how Wirth and Carl first built Lilith then Oberon. Same method will work again and good that ML/Scheme/Oberon folks already gave us doc's plus code to use. Lets use them.
Yep, building up like that would work. Oberon if I recall correctly is pretty simple too (maybe ~20k LOC?) so that would actually be possible by a small team.
Note: LISP/Scheme interpreters and processors with plenty of detail (including source) can be found with Google. Many implemented before 1990. Will run on cheap FPGA's or process nodes. Can take it all the way to hardware. ;)
The macro ASM can be built on something like P-code: an idealized, low-level machine easy to deploy on CISC and RISC architectures. A good example of how to bridge ASM and HLL's is Hyde's High Level Assembly:
So, many possibilities. People just gotta use them. Build a LISP w/ macros to build everything else still seems to be easiest strategy. Esp as one can reuse code from textbooks unlikely to be subverted. Wirth's next best.
Now, I did have a method to solve problem you're addressing. You implement an assembler first. Then a macro assembler with macro's for HLL primitives. You can use that immediately to jmplement certified compiler. Alternately, you can pick up Oberon report or Scheme book to implement that to get a true HLL plus compiler. Then you implememt the certified compiler with it. Comprehension, code complexity, and trust are kept manageable by building layer by layer. This, for productivity not security, is how Wirth and Carl first built Lilith then Oberon. Same method will work again and good that ML/Scheme/Oberon folks already gave us doc's plus code to use. Lets use them.