[cousin_it]

That's correct in theory, but in practice I'd be very surprised to see a useful program that couldn't be verified by ZFC. The only natural way to get such programs is by encoding metamathematics, like trying to verify the consistency of ZFC itself.

[eli_gottlieb]

>That's correct in theory, but in practice I'd be very surprised to see a useful program that couldn't be verified by ZFC.

I think you do too much easy theory if you think that, if you'll excuse my saying so. A lot of the firmware code I write at work is just not going to be formally verifiable in any practical way without scrapping it and rewriting in a language built around formal verification from day one.

Besides which, a Python interpreter is a very common sort of program to write, actually, and I don't expect that you can "just" do the equivalent of `Require Import ZFC` to verify its behavior properly.

[cousin_it]

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

[eli_gottlieb]

>What stops ZFC from proving sentences about Python interpreters, or Brainfuck programs, or whatever?

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 actually matters) also give things that are, let's say, on the research frontier to reason about formally.

And then there's just the fact that ZFC isn't a very good language at all for programming with. Type theories are both proof-theoretically stronger and easier to write something at all like actually programs in.

Also, things like compilers and program analyzers are very common in "real-world" programming. They're just about the cutting edge of what we can do with formal verification today: it helps a lot 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. Then, 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.

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...