4 ms·
Pacemakers, satellites, rocket ships, cars, nuclear plants, etc.
by zeroxfe 9y ago
Pacemakers, satellites, rocket ships, cars, nuclear plants, etc.
- jjjensen90 9y agoThose systems are most definitely not running "untested C code."
- pjc50 9y agoThey're running tested C or Fortran, but there have been at least two rocket losses due to software error. http://www-users.math.umn.edu/~arnold/disasters/ariane.html http://www-users.math.umn.edu/~arnold/disasters/ariane.html https://www.itworld.com/article/2717299/it-management/mariner-1-s--135-million-software-bug.html https://www.itworld.com/article/2717299/it-management/marine...
- riffraff 9y agoAnd they generally have recourse, there are insurance services for rockets, even if you ignore the redundant hardware.
- crankylinuxuser 9y agoMy dad was an automotive engineer for Faruecia (sp?). A lot of emissions code is code he wrote. Wil Crawley , if you look up his 13 or so patents. He did things like the Electronic Muffler (which cancelled exhaust sound with antisound from a hardened speaker). I saw what he did for code review. He didn't "review it". He proved each function, for every input and output. The code he wrote had side effects that only 1 function could write to - and the function was called to change it. And those side effect variables were never critical ones. It was as close to Mathematical Proof as you could get.
- nl 9y agoThis sounds good and all, but there is actually a thing called provable correctness or formal verification, where code really is provably correct. See for example https://ts.data61.csiro.au/projects/seL4/ https://ts.data61.csiro.au/projects/seL4/