 De Millo et al. (1979) question Hoare’s thesis: correct mathematical proofs are usually elegant and graspable, implying that any (expert) reader can “see” that the conclusion follows from the premises (for the notion of elegance in software see also Hill (2018)). What are often called Cartesian proofs (Hacking 2014) do not have a counterpart in correctness proofs, typically long and cumbersome, difficult to grasp and not explaining why the conclusion necessarily follows from the premises. Yet, many proofs in mathematics are long and complex, but they are in principle surveyable, thanks to the use of lemmas, abstractions and the analytic construction of new concepts leading step by step to the statement to be proved. Correctness proofs, on the contrary, do not involve the creation of new concepts, nor the modularity one typically finds in mathematical proofs (Turner, 2018). And yet, proofs that are not surveyable cannot be considered mathematical proofs (Wittgenstein 1956).