NASA has a list of 10 rules for software development

Read the full document (local copy)
or the original.
Read it first, before reading these comments.

Those rules were written from the point of view of people writing
embedded software for extremely expensive spacecraft, where tolerating
a lot of programming pain is a good tradeoff for not losing a mission.
I do not know why someone in that situation does not use the SPARK
subset of Ada, which subset was explicitly designed for verification,
and is simply a better starting point for embedded programming than C.

I am criticising them from the point of view of people writing
programming language processors (compilers, interpreters, editors)
and application software.

We are supposed to teach critical thinking. This is an example.

• How have Gerard J. Holzmann’s and my different contexts affected
  our judgement?
• Can you blindly follow his advice without considering your
  context?
• Can you blindly follow my advice without considering
  your context?
• Would these rules necessarily apply to a different/better
  programming language? What if function pointers
  were tamed? What if the language provided opaque abstract
  data types as Ada does?

1. Restrict all code to very simple control flow constructs —
do not use goto statements,
setjmp() or longjmp() constructs,
and direct or indirect recursion.

Note that setjmp() and longjmp()
are how C does exception handling, so this rule bans any use
of exception handling.

It is true that banning recursion and jumps and loops without
explicit bounds means that you know your program is
going to terminate. It is also true that recursive functions
can be proven to terminate about as often as loops can, with
reasonably well-understood methods. What’s more important here is
that “sure to terminate” does not imply
“sure to terminate in my lifetime”:

    int const N = 1000000000;
    for (x0 = 0; x0 != N; x0++)
    for (x1 = 0; x1 != N; x1++)
    for (x2 = 0; x2 != N; x2++)
    for (x3 = 0; x3 != N; x3++)
    for (x4 = 0; x4 != N; x4++)
    for (x5 = 0; x5 != N; x5++)
    for (x6 = 0; x6 != N; x6++)
    for (x7 = 0; x7 != N; x7++)
    for (x8 = 0; x8 != N; x8++)
    for (x9 = 0; x9 != N; x9++)
        -- do something --;

This does a bounded number of iterations. The bound is N¹⁰.
In this case, that’s 10⁹⁰. If each iteration of the loop body
takes 1 nsec, that’s 10⁸¹ seconds, or about 7.9×10⁷²
years. What is the practical difference between “will stop
in 7,900,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000,000
years” and “will never stop”?

Worse still, taking a problem that is naturally expressed
using recursion and contorting it into something that manipulates an
explicit stack, while possible, turns clear maintainable code into
buggy spaghetti. (I’ve done it, several times. There’s an example
on this web site. It is not a good idea.)

2. All loops must have a fixed upper-bound. It must be trivially
possible for a checking tool to prove statically that a preset
upper-bound on the number of iterations of a loop cannot be exceeded.
If the loop-bound cannot be proven statically, the rule is considered
violated.

This is an old idea. As the example above shows, it is not enough
by itself to be of any practical use. You have to try to make the
bounds reasonably tight, and you have to regard hitting an
artificial bound as a run-time error.

By the way, note that putting depth bounds on recursive procedures
makes them every bit as safe as loops with fixed bounds.

3. Do not use dynamic memory allocation after initialization.

This is also a very old idea. Some languages designed for embedded
work don’t even have dynamic memory allocation. The big
thing, of course, is that embedded applications have a fixed amount of
memory to work with, are never going to get any more, and should not
crash because they couldn’t handle another record.

Note that the rationale actually supports a much stronger rule:
don’t even simulate dynamic memory allocation. You can of
course manage your own storage pool:

    typedef struct Foo_Record *foo;
    struct Foo_Record {
	foo next;
	...
    };
    #define MAX_FOOS ...
    static struct Foo_Record foo_zone[MAX_FOOS];
    foo foo_free_list = 0;

    void init_foo_free_list() {
	for (int i = MAX_FOOS - 1; i >= 0; i--) {
	    foo_zone[i].next = foo_free_list;
	    foo_free_list = &foo_zone[i];
	}
    }

    foo malloc_foo() {
	foo r = foo_free_list;
	if (r == 0) report_error();
	foo_free_list = r->next;
	return r;
    }

    void free_foo(foo x) {
	x->next = foo_free_list;
	foo_free_list = x;
    }

This technically satisfies the rule, but it
violates the spirit of the rule. Simulating malloc()
and free() this way is worse than using the real
thing, because the memory in foo_zone is permanently tied up
for Foo_Records, even if we don’t need any of those at the
moment but do desperately need the memory for something else.

What you really need to do is to use a memory allocator
with known behaviour, and to prove that the amount of memory
in use at any given time (data bytes + headers) is bounded
by a known value.

Note also that SPlint can verify at compile time that
the errors NASA speak of do not occur.

One of the reasons given for the ban is that the performance
of malloc() and free() is unpredictable. Are these the only
functions we use with unpredictable performance? Is there
anything about malloc() and free() which makes them
necessarily unpredictable? The existence of
hard-real-time garbage collectors suggests not.

The rationale for this rule says that

Note that the only way
to dynamically claim memory in the absence of memory allocation from the
heap is to use stack memory. In the absence of recursion (Rule 1), an
upper bound on the use of stack memory can derived statically, thus
making it possible to prove that an application will always live within
its pre-allocated memory means.

Unfortunately, the sunny optimism shown here