I think to require formally proven implementation for something like Java is simply unreasonable. Even if it were possible. The whole computer market, and for that matter, most of the market as a whole, relies on "unproven" products. Most of what you buy and use is based on a notion of "quality" which is merely an inductive argument that the product had no problems in the past. Everytime you buy a piece of software and use it, you risk your security. Everytime you ftp something off the net and run it, you are taking that risk. How do you know MS Word doesn't have security holes or trojan horses built in, have you seen the source? Software always has bugs, holes, and security flaws. It always will. If we were to require each new generation of software to be "formally correct", software would never evolve. There is an important feedback process between customers, software companies, and even hackers, that drives software towards higher quality. Perfect software implementations proven correct by mathematics is a pipe dream. Maybe you can have higher confidence in small, simple software -- I've heard Negroponte expressing that nostalgia for the days of word processors that ran in 32k of ram, but frankly, I'm glad those days are gone. Will the IPv6 and IPSEC stack implementations be formally proven correct? Yes, it may be possible that exploiting holes in Java will be easier than those in sendmail, just as it is easier to exploit a hole in software on a networked machine rather than a non-networked one. But this can not be an argument against Java or its utility. The same arguments were raised when Postscript first came out, yet the huge benefits of postscript are obvious, while the amount of security damage done by it is minimal. Java will have lots of holes. It will go through the same evolutionary progress that all software does. Sendmail was given a chance to evolve, I think Java deserves the same chance, given its potential. -Ray