Andrei's list of barriers to D adoption

[Ola Fosheim Grøstad via Digitalmars-d]

On Wednesday, 8 June 2016 at 00:39:54 UTC, Walter Bright wrote:
> 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.

Well, you cannot prevent errors in the requirements, but you can 
eliminate errors in the proof, so if the requirements are too 
complex  you have a bad deal. The theorem prover is separate from 
the proof verifier. It works like this:

1. Human specifies the requirements (e.g. assert(...) in D)

2. Theorem prover takes program + requirements + strategies 
(prodding the prover along the right track) and emits a loooong 
formal proof in a standard format.

3. The proof is handed to N independently implemented verifiers 
that checks the proof.

But that is impractical for typical user created program. You 
only want to do that once, for your backend or your type-system 
etc.

--

What you can do is, as you've stated before, transform your 
source code into a simpler form and verify that it only can lead 
to situations that are provably safe.

The advantage of this is that you also can prove that specific 
cases of pointer arithmetics are provably safe (say, fixed size 
array on the stack) thus reducing the need for @trusted.

The disadvantage is that it will slow down the compiler and make 
it more complicated, so why have it in the compiler and not as a 
separate program?

Make it a separate program so it works on uninstantiated code and 
prove libraries to be correctly marked @safe before they are 
uploaded to repositories etc.

If @safe does not affect code gen, why have it in the compiler?