Never Mind the Concurrency, What About the Math?

Lots of people are touting functional programming (FP) as a solution to the problem of ever-increasing concurrency. I think the case is “not proven”: I have never seen any trustworthy studies comparing the productivity or post-release fault rate of developers using FP with those using more popular approaches.

What I find more interesting right now is the possibility that wider adoption of FP will help turn software engineering into a real engineering discipline—one whose practitioners routinely use complex mathematics rather than doing proofs about that mathematics. Formal verification tools like SPIN and Alloy are becoming both more powerful and more usable with every passing year; meanwhile, a growing number of developers are learning the hard way that they can’t “code and fix” their way to reliable concurrent software. I wouldn’t be surprised if programmers start adopting functional languages because they are a better target for analysis and proof tools than imperative languages, rather than any intrinsic productivity difference when used traditionally.