My 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.
Comments
Who uses untested C code to control an "oops I just lost $100M and there's no recourse" system?
Pacemakers, satellites, rocket ships, cars, nuclear plants, etc.
Those systems are most definitely not running "untested C code."
My 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.
This 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/
And they generally have recourse, there are insurance services for rockets, even if you ignore the redundant hardware.
They'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
https://www.itworld.com/article/2717299/it-management/marine...