Tony Morris

Reminds me of testing's finding, "All oracles are heuristic". There are no perfect tests that can always separate the working from the not-working.

Yes there are. They are called proofs.

With no side channels?

What is a "side channel"? Proofs show correctness, to the point that there is nothing left to show. It is correct.

After reading the rest of the thread, are you talking about a Lambda Calc proof of an implementation? I'm interested to see an example or two. Side channels from the hardware your implementation runs on make the proof heuristic. On paper it's perfect. On silicon, less so.

They emit information through EMF. They constrain where none exists in the proof. Formally verified algorithms get owned all the time by unseen constraints. That's why all abstractions are leaky and all oracles are heuristic. Gödel's Incompleteness is related.

Here is an abstraction called f. (forall x. x -> f x, forall a b. (a -> f b) -> f a -> f b) Where is the leak?

As lambda calc is a formal logic system, it is necessarily incomplete. Curry's paradox is one example. I can't remember enough lambda calc to do it myself, but how would it handle a contradiction like that?