On 08.06.2016 02:39, Walter Bright wrote:
On 6/7/2016 4:07 PM, Andrei Alexandrescu wrote:
It is my opinion that writing off formal proofs of safety is a
mistake. Clearly
we don't have the capability on the core team to work on such.
However, I am
very interested if you'd want to lead such an effort.
On the contrary, I think a formal proof would be very valuable. I am
just skeptical of the notion that a proof is automatically correct. I've
read about mistakes being found in many published mathematical proofs. I
read somewhere that Hilbert made many mistakes in his proofs, even
though the end results turned out correct.
Mathematicians use a semi-formal style of reasoning in publications.
Most mistakes are minor and most mathematicians don't use tools (such as
https://coq.inria.fr/) to verify their proofs like computer scientists
often do when proving properties of formal systems.
The focus of Mathematics isn't necessarily on verification, it is
usually on aesthetics, understanding, communication etc. Current tools
are not particularly strong in such areas and it is often more tedious
to get the proof through than it should be. And certainly Hilbert didn't
have access to anything like them.
