I generally agree, but formal methods I can say with confidence will get adopted in the future.
Here is why: Testing is fastly becoming adopted by everyone in our industry, why? Becuase you cannot afford to not write tests if your system is large/important enough. However our current testing methods cannot not prove the absence of bugs, as Dijkstra is fond of saying. So the best we can tell our clients currently on the bug-free/security question is this: "We wrote it according to X standard and wrote tests to cover those cases.". Formal methods allow us to prove a system is bug-free/secure. It is the evolution of testing. I do not know how far off it is, but because we have already adopted testing I believe formal methods will get adopted as well.
formal methods don't magically make a specification bug-free/secure though, nor does it mean you won't making bugs in the formal verification code you're writing.. so what are you actually proving? other than just another layer of testing essentially? can anyone tell a client that a system has been 'proven' correct? I think when we use these words with people who don't completely understand the implications we need to be more precise what that means... that's what leslie lamport is all about ! being precise!
Here is why: Testing is fastly becoming adopted by everyone in our industry, why? Becuase you cannot afford to not write tests if your system is large/important enough. However our current testing methods cannot not prove the absence of bugs, as Dijkstra is fond of saying. So the best we can tell our clients currently on the bug-free/security question is this: "We wrote it according to X standard and wrote tests to cover those cases.". Formal methods allow us to prove a system is bug-free/secure. It is the evolution of testing. I do not know how far off it is, but because we have already adopted testing I believe formal methods will get adopted as well.