Point taken. Isn&#x27;t that just a limitation of current tools, though? What stops ZFC from proving sentences about Python interpreters, or Brainfuck programs, or whatever? I&#x27;m not aware of any theoretical roadblocks, apart from the difficulty of actually writing out the proof (which is admittedly huge).