Overconfidence expected

Pascal Cuoq - 9th Dec 2011

I was previously complaining about the use of the word \prove" when describing either what Frama-C or another tool does to mean something other than what it means. But it seems we have come to the point over-confidence is actually expected lest readers get confused. In a submitted article one reviewer pointed out:

The authors themselves are not sure about the quality of the [proprietary] plug-in as "[the proprietary plug-in] SEEMS to produce correct results"

The verb "seems" in the original sentence only means that the proprietary plug-in produces sound results on all the 40000 lines the article documents it has been tried on but that we cannot exhibit a Coq witness of the soundness proof at this time. Anyway since this sentence was confusing it has been changed into a blanket statement of absolute confidence.

Pascal Cuoq
9th Dec 2011