Those are interesting and extremely good ideas, thanks for pointing them out. I do wonder if OpenBSD would accept a C compiler built on a small functional lang

Those are interesting and extremely good ideas, thanks for pointing them out. I do wonder if OpenBSD would accept a C compiler built on a small functional language amenable to these kinds of proofs. I suppose fulfilling the portability requirements is priority one, then stability. I just wonder if they would accept something not written in C at all.