On Fri, 24 Nov 2017, Patrick Meade wrote:

> On 11/23/2017 05:28 AM, Arnt Karlsen wrote:
> > ..aye. And then we have the good old Ken Thompson style compiler
> > hacks and 33 years of water under the bridge to come up with even
> > better hacks...
>
> David Wheeler taught us how to counter Ken Thompson's Trusting Trust attack
> 8 years ago.
>
> https://www.dwheeler.com/trusting-trust/

fantastic post, didn't knew it, thanks! I have been very passionate
about this topic myself for a while now. It wasn't water under the
bridges btw, since many safety-critical and life-critical systems have
mandatory checks to be done on compilers before adopting them into
production, at least in Europe AFAIK.

Another fascinating approach is that of using languages for formal
proof management like Coq. I like to keep my mind occupied thinkering
around stuff like "satisfiability modulo theories" (SMT) and
termination proof. Still coding a prototype around some ideas...

ciao