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.
