> Such a meta-proof must be done on pen and paper, before any code is written at all. Not so fast; it could be done on a _different automated system_ (say, a s

> Such a meta-proof must be done on pen and paper, before any code is written at all. Not so fast; it could be done on a _different automated system_ (say, a smaller one) than the one you're building, in which case you're now relying on that system's correctness. Or it could even not be proven at all. This is not too different from what mathematicians do when they (often) say "assuming P != NP", or "assuming GRH", or "assuming FLT", etc etc. It's simply that it's worth being careful and precise.