Java's memory model places limitations on the extent to which a correctness proof for a program is sound -- whilst it is possible to know a wide class of useful-stuff about a Java program statically, it is not feasible (under normal circumstances) to predict all possible behaviours of the run-time system. This kind of thing makes the people who have to care about safety critical systems more than a little twitchy. I can therefore see exactly where M$ are coming from here, though they do seem to be gloating quite a bit more than is entirely polite, I think, since the same kinds of argument can be made against C, C++ and most other commonly used languages. However, C and C++ *do* support static allocation, which gets around the memory model problem and does allow validation and verification to be attempted, albeit for restricted subsets of the language.
In all cases, this isn't *really* the fault of the languages or the implementations, it's more that people like me haven't figured out how to adequately verify the complete versions of these languages. Of course, it's completely untrue that you *can't* verify Java (NASA's Java Pathfinder project is a clear counterexample, as is their C Global Surveyor abstract interpretation-based static analyser, both of which have been used very successfully on the Mars Exploration Rover mission). It's just that you have to be careful to be realistic about what it is that you've actually *proved*, in terms of the correctness assumptions one makes about the underlying run time environments.
In all cases, this isn't *really* the fault of the languages or the implementations, it's more that people like me haven't figured out how to adequately verify the complete versions of these languages.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
zvi and
no subject
Date: 2006-01-17 10:17 pm (UTC)In all cases, this isn't *really* the fault of the languages or the implementations, it's more that people like me haven't figured out how to adequately verify the complete versions of these languages. Of course, it's completely untrue that you *can't* verify Java (NASA's Java Pathfinder project is a clear counterexample, as is their C Global Surveyor abstract interpretation-based static analyser, both of which have been used very successfully on the Mars Exploration Rover mission). It's just that you have to be careful to be realistic about what it is that you've actually *proved*, in terms of the correctness assumptions one makes about the underlying run time environments.
no subject
Date: 2006-01-18 06:22 pm (UTC)*snort* Rather you than I.