In my opinion, one of the big problems with formal methods is getting the specification right. You might be able to prove that your program conforms to your specification, but what is to say that your specification is any less buggy than your program? Some interesting work has been done with proving that certain errors do not occur, rather than proving the entire program correct. For instance, Microsoft's Terminator project [1] is used to prove that device drivers do not hang.
Comments
In my opinion, one of the big problems with formal methods is getting the specification right. You might be able to prove that your program conforms to your specification, but what is to say that your specification is any less buggy than your program? Some interesting work has been done with proving that certain errors do not occur, rather than proving the entire program correct. For instance, Microsoft's Terminator project [1] is used to prove that device drivers do not hang.
[1] http://research.microsoft.com/en-us/um/cambridge/projects/te...