Andrei's list of barriers to D adoption

Timon Gehr via Digitalmars-d digitalmars-d at puremagic.com
Wed Jun 8 06:39:05 PDT 2016


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.


More information about the Digitalmars-d mailing list