> Sounds like I'm still countering it, though

If you think you could so easily circumvent mathematical theorems, why are you such a believer in formal methods? I don't understand exactly what your method is, but I can assure you you're not circumventing the halting theorem. There's a very precise definition of what it means to be faster. The halting theorem poses no artificial constraints on the problem; it's an extremely general theorem, and it certainly doesn't say how the decision must be made. You're perfectly allowed to serve as an OS and simulate the input program if you like, but that's not going to help.

> How many people looked at it? For how long? And what diversity of backgrounds?

The proof is very simple, and very similar to the proof that a system of cellular automata is Turing-complete: it points out that any nondeterministic Turing machine with a tape of length k cells can be simulated by k finite state machines. If it were possible to verify each component separately and combine the result efficiently, then any such TM could be verified, yet it is well known that it cannot be. The paper was written by well-respected academics, published in a respected journal, and has over twenty citations.

Now, the reason our response should be, "so verification is as hard as we thought", rather than "this is the end of the line", is because, like all results in computational complexity, it talks about the general case. It is possible that a large enough class of programs that are of interest are special cases that are easier to solve.

> Peter Guttman also had a nice rebuttal of reliability of formal methods showing all the times formal specs and proofs were incorrect with it taking years or so for people to spot the errors or disprove it by executing a program.

I don't know what you're referring to, but I'm not aware of any cases where mechanically checked proofs or model checker results have ever been found wrong. The spec can very well be wrong, but you're the one arguing the infallibility of formal methods.

> Preferably a few man-years of people trying to solidify or counter it.

No one is going to try and counter a mathematical theorem, with a very simple, well-understood proof.

> Can you get implicit, global correctness if you decomposed your app into pieces who are each locally correct?

I'm not sure what you mean by "implicit". A formal spec requires a formal proposition to check. Things can be true without us proving them, but formal verification is about verification, not about truth. Theoretically, programs could be correct without verifying or testing them in any way. As to building up a global correctness property end-to-end (from very low-level code and up) is possible by very hard, and no one has ever been able to do it for even medium-sized programs. Obviously, working in a modular way is how people do it; that's how both math and software works. Yet, it's very, very hard.

> Then others and I might learn from your observations.

I think you overestimate my abilities. I'm not an academic. Just a programmer with some experience using formal methods.

> You stay trying to depress us.

This is where you're wrong. Formal methods -- like aviation -- are awesome! But let's enjoy them for what they are, not what we imagine them to be. If you see someone speaking of formal verification as if it were a solved problem, and writing fully correct programs is just a matter of learning Idris, you can know one thing for certain: they've never actually used formal methods on non-trivial real-world programs. The FM experts are those lowering expectations the most. Watch some talks by Xavier Leroy.

> formal specifications, model-checking, test generation

All of these are formal methods (the last only if there's a formal contract).

> http://www.cracked.com/...

:)