|
|
|
|
|
|
by mstevens
5380 days ago
|
|
|
These arguments never quite make sense to me. The reasoning appears to be "since technique X can cause problems in some circumstances, it can never be used in software for domain Y (usually avionics, space, or similar)". However, obviously every technique could cause problems in some circumstances. Therefore I conclude it's impossible to ship software into space. Since software clearly is shipped into space, it seems likely there is some problem with the above argument. My suspect is the "could cause problems? Can't use it!" line of reasoning is oversimplified for the purposes of explanation, and hopefully something better justified is actually occurring. |
|
|
Checking a programmer's claim that a program will not run out of memory is difficult (sometimes impossible) if you allow heap allocations and arbitrary stack usage. You could allow either, if the programmer supplies a proof that things are OK. But with such a proof in hand, writing the thong so that it can be mechanically checked is "just work" (tedious work, possibly, but for this application, that is not that important). Because of that, why risk that such a proof is flawed (or becomes flawed after a bug fix), if one can just as well prevent the problem?
Of course, the checking code will be buggy, too. That is OK; it will be written by a separate team, and will improve over time, just as the code it checks does.
I guess that, even with these checks, the program will still have some watchdog timer, a way to remotely reset it, and a way to upload new software, just in case it runs wild.