As in mathematics, some of the best software research can be very hard for practitioners to recognize, appreciate, learn and apply. Part of the reason is devel

As in mathematics, some of the best software research can be very hard for practitioners to recognize, appreciate, learn and apply. Part of the reason is developers rarely get the opportunity to try out research ideas until enough success stories about them become mainstream. I remember looking into Erlang years ago around the time some folks I knew at Sendmail were looking into it but unfortunately nobody at my company would use it. It was too weird at the time. But if I were working on the same thing today I could easily reassure people by pointing to things like Amazon SimpleDB. These days I'd like to see more mainstream publications about checking and reasoning tools like SPIN[1] and Coq[2] and techniques like Proof Carrying Code[3] so that I can convince my management and peers to try them out. 1- http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html 2- http://en.wikipedia.org/wiki/Coq http://en.wikipedia.org/wiki/Coq 3- http://en.wikipedia.org/wiki/Proof-carrying_code http://en.wikipedia.org/wiki/Proof-carrying_code