> One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this.
"Industry programmers" are pretty far from being a monolith. There are a myriad of different approaches to testing, many of which are ___domain specific, for all kinds of reasons.
Usually the way that a new testing tool gets adapted is that individual programmers or companies that adapt the tool appear to have a competitive advantage over those that don't. The results generally speak for themselves, at least after a time.
Practically everybody that might use formal verification has already chosen to not go to certain lengths to increase reliability. They're already making an economic trade-off -- even with safety critical systems, or in domains where the cost of bugs is extraordinarily high. Why shouldn't formal verification be assessed in the same way?
"Industry programmers" are pretty far from being a monolith. There are a myriad of different approaches to testing, many of which are ___domain specific, for all kinds of reasons.
Usually the way that a new testing tool gets adapted is that individual programmers or companies that adapt the tool appear to have a competitive advantage over those that don't. The results generally speak for themselves, at least after a time.
Practically everybody that might use formal verification has already chosen to not go to certain lengths to increase reliability. They're already making an economic trade-off -- even with safety critical systems, or in domains where the cost of bugs is extraordinarily high. Why shouldn't formal verification be assessed in the same way?