3 ms·

You are right in general where the cost of failing is not that high, but consider software on flights, a pacemaker or (the best example everyone in FM quotes) a

You are right in general where the cost of failing is not that high, but consider software on flights, a pacemaker or (the best example everyone in FM quotes) a space mission. The cost of a small bug can cost you huge money/lifes. In these cases companies have an incentive to verify their code. Hey you don't have to go to these special cases. Amazon, google, Microsoft all do Formal verification (or have started somewhat sophisticated testing) of their critical pieces of code as a bug in them even if it causes an hour of downtime will cost them in millions.

p1necone 8y ago
But most software is not on flights, pacemakers or space missions (or equivalent).
- joe_the_user 8y ago
  Indeed, under those circumstances, yeah formal and semi-formal methods get used. But since these circumstance aren't common [goto: very eloquent GP].
- Tempacc78534 8y ago
  It's a cost benefit analysis, if the failure costs you more than verifying it then you will verify it. Since cost of verification is currently high, if you are not losing millions due to failure it doesn't make sense to verify your code. Look at fuzzing. No one did fuzzing a decade ago. Since fuzzing became cheap (i.e. due to cheap compute and somewhat due to cloud computing) everyone does fuzzing on pieces of code which remotely appear to be critical. Even testing. When cost of running a program was high people didn't write test cases. They hand checked programs for bugs.
hwayne 8y ago
I didn't include it in the article because I wasn't 100% confident in saying so, but I'm reasonably sure that medical devices don't use FM. There's not a whole lot of oversight in that area, and most of the standards are (to my knowledge) about software process versus software methods. Aviation also doesn't really use FM, but that's because they follow DO-178C, and that is a scary scary standard.
- Tempacc78534 8y ago
  It would way cheaper for them to verify their code than to probably follow these standards but bureaucracies are bureaucracies. Also, a little nitpicking in your write up but you should have also talked about type systems. They carry the spirit of formal methods but rather than being construct then check for correctness, are construction is correct by default. Type systems are widely accepted and show that some of these ideas can gain traction.
- tnecniv 8y ago
  I don't know how it's used in practice, but aviation companies dump a lot of money into formal methods research because getting their code certified to meet scary specs is very expensive and they don't want to do it for every bug fix.
- mcguire 8y ago
  I haven't been anywhere near it, but DO-178C is allegedly friendly to formal methods; DO-333 is the formal methods supplement. Adacore had a white paper, "Testing or Formal Verification: DO-178C Alternatives and Industrial Experience" that naturally I can't link because I'm on mobile.

p1necone 8y ago

But most software is not on flights, pacemakers or space missions (or equivalent).

joe_the_user 8y ago
Indeed, under those circumstances, yeah formal and semi-formal methods get used. But since these circumstance aren't common [goto: very eloquent GP].
Tempacc78534 8y ago
It's a cost benefit analysis, if the failure costs you more than verifying it then you will verify it. Since cost of verification is currently high, if you are not losing millions due to failure it doesn't make sense to verify your code. Look at fuzzing. No one did fuzzing a decade ago. Since fuzzing became cheap (i.e. due to cheap compute and somewhat due to cloud computing) everyone does fuzzing on pieces of code which remotely appear to be critical. Even testing. When cost of running a program was high people didn't write test cases. They hand checked programs for bugs.

hwayne 8y ago

I didn't include it in the article because I wasn't 100% confident in saying so, but I'm reasonably sure that medical devices don't use FM. There's not a whole lot of oversight in that area, and most of the standards are (to my knowledge) about software process versus software methods. Aviation also doesn't really use FM, but that's because they follow DO-178C, and that is a scary scary standard.

Tempacc78534 8y ago
It would way cheaper for them to verify their code than to probably follow these standards but bureaucracies are bureaucracies. Also, a little nitpicking in your write up but you should have also talked about type systems. They carry the spirit of formal methods but rather than being construct then check for correctness, are construction is correct by default. Type systems are widely accepted and show that some of these ideas can gain traction.
tnecniv 8y ago
I don't know how it's used in practice, but aviation companies dump a lot of money into formal methods research because getting their code certified to meet scary specs is very expensive and they don't want to do it for every bug fix.
mcguire 8y ago
I haven't been anywhere near it, but DO-178C is allegedly friendly to formal methods; DO-333 is the formal methods supplement. Adacore had a white paper, "Testing or Formal Verification: DO-178C Alternatives and Industrial Experience" that naturally I can't link because I'm on mobile.