> C is one of the worst possible foundation languages conceivable for > automated formal verification
Yet the Mars rovers run on a wholly checked code base written in C, subject to certain mechanically enforced restrictions on coding style. I'm not aware of comparably challenging systems having been verified regardless of programming language. But I stray far from groff. Doug
