Shops that use strongly-typed functional languages are, in my experience, a good bet. They usually made that choice because they have an unusually compelling need to write correct code. Aerospace also has a few sub-industries where correctness is priority #1 (like commercial autopilot software).

Probably the Apollo moon lander software team, circa 1968.

This article bothers me because it implies that the path to correct code is simply to have code written by white-collar salarymen (as opposed to unkempt youth), and not improved formal methods.

It doesn't imply there is a correct path to code. It implies that the best path to the goal for this program is to minimize the opportunity for exhaustion to be a variable.

> That’s the culture: the on-board shuttle group produces grown-up software, and the way they do it is by being grown-ups. It may not be sexy, it may not be a coding ego-trip — but it is the future of software. When you’re ready to take the next step — when you have to write perfect software instead of software that’s just good enough — then it’s time to grow up.

It might not be the future of software, but it's the software of the future, in the sense that it's what enabled us to get to the moon, and will enable us to get to Mars.