|
I would think the reasoning would be "pick the low-hanging fruit to improve reliability". 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. |
Indeed.
As for the reasoning: couldn't have said it better myself.