|
|
|
|
|
|
by cousin_it
3939 days ago
|
|
|
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). |
|
|
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...