Andrei's list of barriers to D adoption
Timon Gehr via Digitalmars-d
digitalmars-d at puremagic.com
Tue Jun 7 15:23:33 PDT 2016
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.
More information about the Digitalmars-d