I like to program but as I get older I am less and less happy about the fragile nature of code. I firmly believe that if you have the right people you should invest in more formal aproaches to software development. The tricky part is there are not enough people that understand that any gap in invariant properties at one layer of software will corrupt the layers above. Languages like C++, Java, C# oblige the developer to choose a subset of the language to build a robust core and then to extend it with limited features of the language. This is fundementally a difficult thing to do and why I spend much time thinking in term of functional languages like scheme, haskell, ocaml because they are not corupted languages.
A note that a good way to learn functional languages is to start with Q: http://q-lang.sourceforge.net/ , a simple term rewriting language. Its easy to setup and use.
Personally, I prefere a term rewriting anotation to a lambda based notion to write programs.
This said look at http://www.galois.com/ , these guys have understood what I am talking about.