I spent some time working with the people at the advanced computation group there. It was a short time, and it was all in the formal systems/automatic analysis

I spent some time working with the people at the advanced computation group there. It was a short time, and it was all in the formal systems/automatic analysis area, so this is a summary of what I picked up within my limited view... The thing is that software's taken at a very different angle from there as in most parts. First, the ones who know exactly what's supposed to happen aren't software people, they're engineers who don't write code. At least not real-time embedded control code. Second, there are too many different people who's interests come together in the same codebase. I.E. lots of different engineering disciplines at once. Each one has their own work to do separate from the programming. You can get specifications & equations out of them, but the code's a different group. Third, the need for high assurance is important. Note the word 'Assurance.' If something bad happens at Nasa, there's a lot of news and possibly a statement by The President. Being that this is a government agency building stuff, it's going to have similar problems to DoD agencies building stuff. That is, an incredible amount of the project will be spent to reduce the variability of the project. Even if the sum cost is many [, many]* times the likely variance. The main space they have to work with is in mechanized assurance systems. Sadly, the formal systems out there aren't terribly evolved, as most people just test & debug their systems to get it right. As for contributions to software, or lessons learned, there are some very good experiences & things learned for people who want to build better tools to make this stuff easier. E.g. higher-level languages that look more like Matlab than embedded C (don't get me started on Matlab-C converter). Stuff where you can be sure that no matter what instruction sequences you give to a robotic arm, that it never ends up in a position where one of joints is locked. When I was there, the attempt was natural language to CSP traces, to be run through a theorem prover there later. We had a total of two grad students working on it over a summer, after an initial prototype was written earlier. As other posts on HN have mentioned, and as one can surmise from the chatter about Nasa, it's costs are very closely looked at by a lot of people -- many who don't understand/know/care about the specific problems Nasa's got. That creates a whole new set of problems. Being observed under a microscope and then being hit for everything a nontechnical senator can get political points for hitting you for will make you start working in pretty strange ways.