Andrei's list of barriers to D adoption

[Timon Gehr via Digitalmars-d]

On 07.06.2016 22:36, Walter Bright wrote:
> ...
>
> BTW, it is a nice idea to require mathematical proofs of code
> properties, but real world programming languages have turned out to be
> remarkably resistant to construction of such proofs. As I recall, Java
> had initially proven that Java was memory safe, until someone found a
> hole in it. And so on and so forth for every malware attack vector
> people find. We plug the problems as we find them.

Obviously they proved the virtual machine itself memory safe, not all of 
its implementations. If you have a mechanized proof of memory safety, 
then your language is memory safe.