Indeed, if memory serves (it's been a while since I read about this)...
The fly-by-wire flight software for the Saab Gripen (a lightweight
fighter) went a step further. It disallowed both subroutine calls and
backward branches, except for the one at the bottom of the main loop.
Control flow went forward only. Sometimes one piece of code had to leave
a note for a later piece telling it what to do, but this worked out well
for testing: all data was allocated statically, and monitoring those
variables gave a clear picture of most everything the software was doing.
The software did only the bare essentials, and of course, they were
serious about thorough ground testing.
No bug has ever been found in the "released for flight" versions of that
code.
Henry Spencer
[email protected]