&gt;What stops ZFC from proving sentences about Python interpreters, or Brainfuck programs, or whatever?<p>Well, mostly a lack of writing down axioms about how these things actually work.  The innate nondeterminism, imperative operating environment, and intentional behavior (in the sense that which implementation of a function you write <i>actually matters</i>) also give things that are, let&#x27;s say, <i>on the research frontier</i> to reason about formally.<p>And then there&#x27;s just the fact that ZFC isn&#x27;t a very good language at all for programming with.  Type theories are both proof-theoretically stronger <i>and</i> easier to write something at all like actually programs in.<p>Also, things like compilers and program analyzers are <i>very</i> common in &quot;real-world&quot; programming.  They&#x27;re just about the cutting edge of what we can do with formal verification today: it helps <i>a lot</i> that, as I understand things, when you write down an inductive type in a dependently-typed proof assistant, you are also writing down axioms (an induction principle) with which to prove theorems about it, and the dual for coinductive types.  <i>Then</i>, between coinductive and inductive proofs that rely on either productive nontermination or eventually-terminating programs, we can write down most of what we actually want to code.<p>With the exception, of course, of proof assistants, where we can still only write a verified implementation of one system using a strictly stronger system.  Gosh, if only someone was working on ways to tie that knot...