"Gerard Holzmann External Link was a keynote speaker at OOPSLA today. Gerard is a fellow at NASA's Jet Propulsion Laboratory (JPL) External Link in Pasadena, California, and has done a great deal of software development for spacecrafts. It is indeed very interesting to see how NASA makes sure that their multi-million dollar space missions are not jeopardized due to programming glitches." - imabonehead from Bookmarklet

"Gerard pointed out some interesting statistics on spacecraft software. The first moon lander in 1969 had a system equivalent to about 10,000 lines of code. By the estimates, the next Lunar mission to come in 2019 would have about 10 million lines of code! We would surely have the necessary hardware technologies to handle such a system, but it is inevitable that the number of defects also increase with such a large system. In Gerard's own words "the human brain is not going to get bigger that soon" and at current rate about two residual defects are found per 1000 lines of code. Geralds guiding principle is "if we don't learn to use computers to analyze our programs, we are in a losing battle." - imabonehead

"The lessons from JPL are equally applicable to today's software development processes. The cost of formal verification, both in terms of time and effort, have come down and at the same time failures are becoming costlier than ever. Perhaps it's time for us to take a lesson from NASA?" - imabonehead

JPL has done a lot of cool work on embedded architectures for autonomous space craft. - Todd Hoff

Formal verification will be a really hard sell in industry. In some build systems I've worked on I've included automated checks and integrated in automated code reviews that integrated in with source code control, testing, source code control, etc, and even that was looked on unkindly. - Todd Hoff