Saturday, January 10, 2015

Does and explanation or an experiment qualify as a formal proof?

The short answer is no. Read on.
 
A formal proof is a sequence of sentences, starting from axioms, and developing using rules of inferences. Details are here: http://en.wikipedia.org/wiki/Formal_proof .
An experiment is not a formal proof. A formal proof is deductive while an experiment is inductive. Deduction is the method of inference in formal, rigorous models, such as math, computer science, and logic. While induction is the method of inference in observation-based models, such physics, biology, and chimestry (and similar fields). Induction cannot give useful and trustworthy information except if quantified correctly. The usual method of quantifying induction is through statistics (and more recently, machine learning). Experiments are mostly used in applied fields, where it suffices (and is possible) to show that something occurs. However, it is impossible to use experiments to show that something does not occur. In particular, it is impossible to show, using experiments, that a system is secure; since it is equivalent to showing that something bad does not occur.

Explanations are something different. Explanations are just a theory. Some of them may be tested, if they were falsifiable (testable, if you wish). But to the uninitiated, they can be very deceiving. Just because you can explain something, does not mean you proved it. An explanation just shows that something is plausible. But does not show that it is unavoidable. There is a cognitive bias known as confirmation bias (look it up) that say we are more likely to believe things that we can explain; which leads to serious logical fallacies. Therefore, a true scientist (going through masters and PhD) is trained to challenge his believes by trying to prove their opposite. Which is why in statistics we are usually interested in the null hypothesis instead of what we are actually trying to show. However, this is still more related to the inductive branch of inference, not the deductive branch.
In computer science, and in particular security and cryptography, deduction is the only way to show that we have an interesting result. This is why a formal proof is need, and why an explanation or an experiment is not. This is more serious that you can imagine; understanding this distinction is what makes a true scientist from a layperson.