Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.



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.


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.


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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: