These real-world programs that no one is willing to use formal proof tools on are 2-5 orders of magnitude more complicated than the hypothetical proof checker under consideration would be.
These real-world programs that no one is willing to use formal proof tools on are 2-5 orders of magnitude more complicated than the hypothetical proof checker under consideration would be.