AFAIK, that is true. I am not aware of any ocap *languages* that attempt to address this.

Non-distributed platforms, yes. All the members of the KeyKOS family (KeyKOS, EROS, GuardOS, CapROS, Coyotos) do/did a brilliant job at this.

Inherent in their approach, the kernel does no implicit allocation. All are based on rendezvous rather than asynchronous messages, and so no kernel buffering of messages is implied.

Distributed defensive correctness over unreliable networks is, almost by definition of "unreliable", impossible.

This suggests defining some possible approximations to defensive correctness:

* Distributed defensive correctness in the absence of spontaneous partitions or crashes, where "spontaneous" means, not caused by the actions of the programs we are concerned with.

* Defensive correctness up to resource exhaustion, which corresponds to the traditional concept of "liveness". Since this concept is well known in the literature, you may at least want to mention it, even if only to dismiss it.

* Budgeted and preemptively reclaimable resource allocation, in order to isolate the effects of resource exhaustion. For example, if we run a KeyKOS-like system but run only dynamically allocating languages -- or languages with no contract regarding resource use -- within each KeyKOS-like process, then an individual KeyKOS like process can still not be defensively correct, because we can't reason about if it will run out of storage while serving a valid request from a valid client. However, if it does, it only exhausts its own storage and thereby fails to service only its own clients. And it can't prevent the reclamation of its storage by an adequately authorized subject.
 

To be meta-hyper-turbo-pedantic, I claim this is false. A program is correct only if it relies only on specified properties of its platform, and not on unspecified properties of its platform's implementation. The specified semantics of all these languages either
1) assumes away the possibility of memory exhaustion, in which case their specification is not implementable (or only implementable up to fail-stop, which is inadequate for progress guarantees), or
2) they allow an out of memory condition to occur any step of computation that may allocate memory, including function/method calls in languages that allow recursion.

In either case, even a program as simple as

    function main() { foo(); }
    function foo() { print("hello world"); }

as expressed in almost any language in use today cannot be said to correctly implement the spec "prints 'hello world'." The most that can be said is that it will either do so or it will run out of memory. In Fortran 4, Occam, or any of the bare handful of languages without recursion or implicit dynamic allocation, given an appropriate and realizable spec, we can at least say that the above program will either fail to load or correctly run to completion. In these languages, one can write programs that would be defensively correct *given* that they successfully load. This is another useful approximation of defensive correctness -- perhaps the closest practical one.

 

Not "ensure", but to defend to an often practical degree. The approximations to defensive correctness I enumerated earlier in this thread derive from thinking about such practical defenses.

My section 5.7 "A Practical Standard for Defensive Programming" includes:

Defensive progress up to resource exhaustion, where we include non-termination,
such as an infinite loop, as a form of resource exhaustion. Protocols that achieve
only defensive progress up to resource exhaustion are normally regarded as satisfying
a meaningful liveness requirement. Whether this standard is usefully stricter than
cooperative progress we leave to the judgement of the reader.