This article applies mathematical logic to obtain a rigorous foundation for previous inherently nonrigorous results and also extends those previous results. Roughly speaking, our main theorem states: any agent A that comprehends the correctness-related properties of software S also comprehends an intelligence-related limitation of S . The theorem treats the output of S , if any, as an attempt at solving a halting problem. Previous nonrigorous attempts to obtain similar theorems depend on infallibility assumptions on both the agent and the software. The hypothesis that intelligent agents and intelligent software must be infallible has been widely questioned. In addition, recent work by others has determined that well-known previous attempts use a fallacious form of reasoning; that is, the same form of reasoning can yield paradoxical results. Our main theorem avoids infallibility assumptions on both the agent and the software. In addition, our proof is rigorous, in the sense that in principle one can carry it out in Zermelo-Fraenkel set theory. The software correctness framework considered in the main theorem is that of Hoare logic.

Associativity is required for the use of general scans and reductions in parallel languages. Some systems also require functions used with scans and reductions to be commutative. We prove the undecidability of both associativity and commutativity. Thus, it is impossible in general for a compiler to check for those conditions. We also prove the stronger result that the resulting relations fail to be recursively enumerable. We prove that these results hold for the kind of function subprograms of practical interest in such a situation: function subprograms that, due to syntactical restrictions, are guaranteed to halt. Thus, our results are stronger than one can obtain from Rice's Theorem. We also obtain limitations concerning the construction of functions and limitations concerning compiler-generated run-time checks. In addition, we prove an undecidability result about programmer-constructed run-time checks.

The multiway rendezvous is a natural generalization of the rendezvous in which more than two processes may participate. The utility of the multiway rendezvous is illustrated by solutions to a variety of problems. To make their simplicity apparent, these solutions are written using a construct tailor-made to support the multiway rendezvous. The degree of support for multiway rendezvous applications by several well-known languages that support the two-way rendezvous is examined. Since such support for the multiway rendezvous is found to be inadequate, well-integrated extensions to these languages are considered that would help provide such support.