It's quite feasible. You just pay a programmer or smart student to do it for you using the published literature. Done. Even stronger if you trust them. Use multiple, distrusting pros on same project if more trustworthiness is needed. What you cant afford you crowd fund or ask for grants.
It's a question of priorities rather than feasibility. Most users or customers dont care enough to invest time or effort needed. End of story. Same one as usual for strong INFOSEC.
I'll also add that there already exists certifying compilers for C and Standard ML that both extract to ML. The ML extracted is simple enough to hand-compile to ASM following one of two guides. So, not only can oma human verify no subversion, there's already a production one with machine-checked proof that's also be checked by humans [again].
It's a question of priorities rather than feasibility. Most users or customers dont care enough to invest time or effort needed. End of story. Same one as usual for strong INFOSEC.
I'll also add that there already exists certifying compilers for C and Standard ML that both extract to ML. The ML extracted is simple enough to hand-compile to ASM following one of two guides. So, not only can oma human verify no subversion, there's already a production one with machine-checked proof that's also be checked by humans [again].