Provably considered harmful
This is officially a rant and should be read as such.
Here is my pet peeve: theoretical computer scientists misuse the word “provably”. Stop it. Stop it!
Theoretical computer science is closer to mathematics than it is to computer science. There are definitions, theorems and proofs. Theoretical computer scientists must understand mathematical terminology. The words “proof” and “provable” are in the domain of mathematical logic. A statement is provable if it has a proof in a given formal system. It makes no sense to say “provable” without specifying or implying a specific proof system.
But theoretical computer scientists say things like (I just googled these randomly) “A Provably Optimal Algorithm for Crowdsourcing” and “A Provably Correct Learning Algorithm for Latent-Variable PCFGs” and even “provably true”.
So what is a “provably optimal algorithm” ? It is an algorithm for which there exists a proof of optimality. But why would you ever want to say that in the title of your paper? I can think of several reasons:
- You proved that there exists a proof of optimality but did not actually find the proof itself. This of course is highly unlikely, but that does even not matter, for as soon as we know there exists a proof, the algorithm is optimal. Just say “optimal algorithm” and the world will be a more exact place.
- Your paper is an intricate piece of logic which analyzes existence of proofs of optimality in some super-important formal systems. This of course is not what theoretical computer scientists do for the most part. Any paper which actually did this, would instead say something like “$\mathrm{Ind}(\Sigma^0_1)$-provability of optimality”.
- You distinguish between algorithms which are optimal and those which are optimal and you proved they're optimal. In that case we should turn tables: if you ever publish a claim of optimality without having proved it, put that in your title and call it “Unproved optimal algorithm”.
- You proved that your algorithm is optimal, showed the proof to the anonymous referee and the editor, and then published your optimal algorithm without proof. You want to tease your readers by telling them “there is a proof but it's a secret”. If this is what you meant to convey, then the title was well chosen.
To see that “provable” is just a buzzword, consider what it would mean to have the opposite, that is an “unprovably optimal algorithm”. That is an algorithm which is optimal, but there exists no proof of optimality. Such a thing can be manufactured by a logician, probably, but is certainly not found in everyday life.
As someone is going to say that “provably true” makes sense, let me also comment on that. A statement is true if it is valid in all models. So “provably true” would mean something like “there exists a proof in a given formal system that the statement is valid in all models”. Well, I will not deny that a situation might arise in which this sort of thing is precisely what you would consider, but I will also bet you that it is far more likely that “provably true” should just be replaced by either “provable” or “true”, depending on the particularities of the situation.
As a rule of thumb, unless you are a logician, if you feel like using the word “provably”, just skip it.
And as long as I am ranting, please stop introducing every single concept with “informally” and prefixing every single displayed formula with “formally”. Which is it,
- you think that “informal” descriptions are somehow unworthy or broken, and you should therefore alert the reader that you're lying to them, or
- you think that “formal” descriptions are an unnecessary burden which must be included in the paper to satisfy the gods of mathematics?
If the former, stop lying to your readers, and if the latter stop doing theoretical computer science.
Now I will go on to refereeing that pile of POPL papers which must contain at least a dozen misuses of “provably” and two dozen false formal/informal dichotomies.
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
I usually refer to "informal" proofs as proofs which are written in words, and "formal" proofs as proofs which are written in a proofchecker (Coq, Minlog, Isabelle, etc.). But this only makes sense when this difference is in the scope of a paper. On the other hand, there are many papers out there about data structures which are claimed to be "optimal" because of benchmarks or vague handwaving.
I think then perhaps you should say "formalized" proofs? In any case, using "formal" to actully mean formal is of course ok!
Are you saying they let people publish claims of optimality based on handwaving? Then we should have a third category of "suspected optimal proofs". It is inexcusable that people who actually prove their claims need to emphasise that they did it. The others should be made to qualify their claims as "unproved".
You are on the programme committee of CCC 2015, whose advertisement contains the following sentence: <blockquote>The overall aim is to apply logical methods in these disciplines to provide a sound foundation for obtaining exact and provably correct algorithms for computations with real numbers and related analytical data, which are of increasing importance in safety critical applications and scientific computation.</blockquote> None of your four proposed reasons for using the word "provably" seems to apply to this text.
I also disagree that "provably" has always to be interpreted in the sense of mathematical logic with respect to a given formal system. My only requirement would be that if you use the word "provably" in the title, then already the abstract should make it clear why you use it, and what it means in your context. It could mean that the proof relies on some assumptions which are widely believed to be true, for example.
Dear Thomas: good catch! I did not write that advertisment, but I will ask, as a member of PC, for the word provably to be removed. We'll see how it goes.
I disagree with you about the use of words. Appropriating a standard phrase from one area of science and altering it slightly (or not so slightly) is impolite, and it creates confusion unecessarily. But what are all these other uses of "provably" that you have in mind?
I can imagine many reasons to label a statement as "provable" instead of as "true". For example, simulated annealing provably converges towards the global optimum. Here the qualification "provable" allows to separate a well defined theoretical truth from the ambiguous practical consequences of the truth. So "provable" is indeed used as an euphemism here, but who is to blame for the ambiguous practical consequences of theoretical truths (for black box optimization)?
A proof can also be part of the process to convince somebody of a certain fact. But the proof might only be convincing to the specific person to which it was delivered. So Jesus delivered proof that convinced doubting Thomas of the resurrection, but a reader of the bible cannot get the same degree of certainty from that proof as did Thomas (for obvious reasons). This sort of proof sometimes allows "the verifier" (i.e. doubting Thomas) to make the remaining doubt as small as desired (say exp(-42) to fix some order of magnitude) by repeated queries, but note that even if he could reduce the remaining doubt to 0, the fact might still not be true.
Under certain assumptions, this type of proof with arbitrary small remaining doubt can even apply to mathematical statements. Take a sufficient non-trivial identity for example (or a prime number if you prefer), which has been checked by "the verifier" by sufficiently many random tests to ensure that the remaining doubt is below exp(-421) (or maybe just below 2^-29, it is subjective to a certain degree). Only "the verifier" can know that his random tests were sufficiently random, and even he cannot be absolutely sure. Sometimes you don't even require true randomness for this type of scenario, take for example Freeman Dyson conjecture that the reverse of the decimal representation of a power of two is never the decimal representation of a power of five.
But I didn't really care about the actual possible meanings of "provable" too much, I just don't want to impose arbitrary limits on the language used in mathematical papers. But I expect that authors make it clear what they mean when they use "provable" outside of a well established context, precisely because I can imagine so many possible uses of that word.
I do not care much about what Jesus proved, but withint he domain of mathematics and mathematical papers, I would not really say that I am "setting arbitrary limits" when I ask that people use the word "provable" with its established meaning, which is "has a proof".
If anyone wants to express "lesser" degrees of proof then they shlould qualify them, be it "practically true", "true by experience" or "probabilistically provable".
You expect that authors explain the word "provable" if they use it in a non-standard way. But my observation is that they do not, and they use it without thinking because it has become part of jargon in theoretical computer science. It is a buzzword which means nothing when used this way. And this is bad.
I think in the context "to apply logical methods ... to provide a sound foundation for obtaining ... provably correct algorithms", the use of "provably" is correct, for two reasons. First, it falls under the "unless you are a logician" exception. What the sentence seems to be saying is "we need solid logical foundations so that we can prove the correctness of algorithms", and not just "we need solid logical foundations so that we can develop correct algorithms". I assume one of the purposes of the logical methods and solid foundations is to enable the activity of proving.
The second reason is that it is okay, in my opinion, to use the word "provably" in negative positions (i.e., on the left-hand side of an implication). An example of a negative occurrence is: "The goal is to have a provably correct algorithm". Or more explicitly: "If we had a provably correct algorithm, then we'd have reached our goal". There seems to me to be a clear difference between "I want my algorithm to be correct" and "I want to be able to prove it".
In positive statements, it is more iffy. I agree that it is mostly redundant to say in the title of your paper that it contains a "provable theorem". It would be equally silly to say that it contains a "true theorem". On the other hand, redundancy is not always a bad thing, depending on who might be the audience. In many parts of non-theoretical computer science, heuristic algorithms might be the norm, and testing might be an accepted means to establishing correctness, so someone might want to say that their algorithm is "provably correct" to emphasize that point and to set themselves apart from that community.
Also, if I say "I cannot solve 3-SAT in polynomial time", it's just a statement of personal inadequacy, but if I say "I provably cannot solve 3-SAT in polynomial time", it's a revolutionary claim.
@PeterSelinger: I am mostly ranting about the fact that it is an empty buzzword for a large chunk of computer science community. Of course there will be cases where it is appropriate to use "provably". I disagree a little bit with your examples because you say "provable" (implying it could be proved but maybe it was not) and "proved". For instance: "If we proved our algorithm to be correct then we'd reach our goal" seems better than "If there existed a proof of correctness of our algorithm then we'd reach our goal", and the latter is equivalent to "If we had a provably correct algorithm then we'd reach our goal".
I am all for clarity and against buzzwords. But I am also against researchers who believe they own words. Your summary 'unless you are a logician, if you feel like using the word “provably”, just skip it', is exactly that. "People, this is our word.. you don't get it, please let us grown-ups alone use it".
Assume you work in an empirical field, and all algorithms so far to solve problem X are just heuristics who happen sometimes to find the optimal solution. Now, researcher Y comes up with an algorithm that solves X always... how would you title it? "Correct algorithm for X"? Well, the others were 'correct' for the people in the field in the sense that it may have been good enough. Including provably indicates that you have a theoretical proof, which not all papers in CS have.
Well, as I stated already, this is a rant. People who are close to logic should know better. People who work in algorithmics have a real need for a word that says "I actually proved that this thing does what it does". It's unfortunate that they picked "provably" because that makes it sound as "it's possible to prove that this thing does what it does", but I of course understand that they'll keep using it. If I had it my way, I would require all those heuristics to be qualified as "heuristically" or "experimentally" or some such, and then I would not need any words for the case with proofs. So, instead of "Optimal sorting aglorithm" and "Provably optimal sorting algorithm" we would have "Heuristically optimal sorting algorithm" and "Optimal sorting algorithm", respectively. After all, if the title of a paper makes a claim, say "Bananas are yellow" people expect the paper to demonstrate that bananas are yellow. In computer science, to demonstrate a property of an algorithm is to prove that property, because algorithms are mathematical objects. If the property is not actually proved, but rather experimentally verified, then the title should say so. But I realize that this is the point of view of a mad mathematician.