Skip to content
Hamilton Archive
0 / 17
Pre-launch Review

HOS Conference Papers (1974, 1978)

This page collects two shorter HOS-era conference papers that bookend the foundational period: the 1974 Springer paper that first published the axioms, and the 1978 COMPSAC paper that grounded reliability in definition rather than testing. Together, they show Hamilton and Zeldin moving from Apollo practice to formal theory to applied philosophy.

Higher Order Software Techniques Applied to a Space Shuttle Prototype Program (1974)

Section titled “Higher Order Software Techniques Applied to a Space Shuttle Prototype Program (1974)”

The Bridge from Apollo to Formalism

Section titled “The Bridge from Apollo to Formalism”

Margaret H. Hamilton and Saydean Zeldin, Charles Stark Draper Laboratory, 1974

HOS is defined as “software expressed with meta-software and conforming to a formalized basic set of laws.” The paper opens with an analogy: mathematics has its own formalization and metalanguage, yet software has been developed without equivalent formal laws. HOS begins with problem formulation and ends with verified code.

Hamilton and Zeldin describe how the Apollo on-board software executive was asynchronous, provided multi-level man-machine interface, and achieved sophisticated error detection and recovery. They note: “No known errors in the on-board software system occurred during all of the APOLLO and Skylab space flights.” However, the cost of approaching this reliability was excessive — motivating the search for formalization.

The Unified Module Problem

Section titled “The Unified Module Problem”

The critical insight comes from the Space Shuttle prototype. When multiple mission phases invoke the same navigation module with different sub-module requirements, the module becomes “unified” — meaning any change to it requires retesting all callers. Hamilton contrasts the unified approach (embedding switching logic within shared modules) with HOS control (each mission phase invoking only the specific subfunctions it needs). This separation of control from function is the key architectural principle.

The Six Axioms

Section titled “The Six Axioms”

The formal control system is defined as a tree where each node represents a unique point of execution. The six axioms governing invocation, responsibility, output access rights, input access rights, rejection of invalid inputs, and ordering are presented here for the first time.

The paper makes an unusual appeal to Russell’s Paradox to motivate the prohibition on self-controlling modules: “Suppose S to be the set or class of sets which are not elements of themselves.” Just as the paradox arises from unrestricted self-reference in set theory, uncontrolled recursion in software produces analogous contradictions.

Key theorems include: no circular invocation (Theorem 1.1), no extraneous functions (Theorem 1.2), a process cannot interrupt itself (Corollary 6.4.4), the WAIT statement is inconsistent with the control system (Lemma 6.4.4.1), and maximum completion time can be computed for any process (Theorem 6.10).

The Grand Theorem

Section titled “The Grand Theorem”

“It is possible to control all functions of any given software problem such that one controller controls all functions.” This proves that HOS is universal — any software system can be expressed within the axioms.

The Shuttle Application

Section titled “The Shuttle Application”

The Shuttle on-board flight software prototype served as the testbed. Three development phases were defined: (1) general problem definition independent of hardware; (2) algorithm definition for computer functions; (3) architectural evolution including hardware aspects. The HAL language provided basic constructs. Functional control maps and structured flowcharts guided development.

Reliability in Terms of Predictability (1978)

Section titled “Reliability in Terms of Predictability (1978)”

Reliability Is Predictability

Section titled “Reliability Is Predictability”

Margaret H. Hamilton and Saydean Zeldin, Higher Order Software, Inc., 1978

The central thesis: “A reliable system is a predictable system; it does exactly what it is intended to do.” Reliability depends on how error-free a system is. But the paper immediately problematizes this by asking: what is a system? what is an error? what does it mean for a system to have an error?

Hamilton defines a system as “an assemblage of objects united by some form of regular interaction or interdependence” where a system could itself be an object within another system. She identifies four viewpoints of any system: (1) definition — what it is supposed to do; (2) description — whether the definition is effectively conveyed; (3) implementation — whether it is constructed correctly; (4) execution — whether it does what it is supposed to do.

The critical point: “If it is not possible to properly identify the object in question, we could be discussing different objects when we think we are talking about the same ones.” Without formal definitions, even the question “was there an error?” cannot be objectively answered.

Socratic Q&A from Apollo Experience

Section titled “Socratic Q&A from Apollo Experience”

The heart of the paper is a series of questions and answers drawn directly from Apollo experience:

“What is a software error?” An unintended phenomenon in either the specification or the computer program. Two kinds: self-contained (internal inconsistencies) and cross-layer (specification vs. implementation mismatches). The Apollo data: 75% of development errors were logical incompleteness or inconsistency; 13% were cross-layer.

“If the computer program doesn’t work because the specification is wrong, is the computer program unreliable?” The software was unreliable if the specification was unreliable. With respect to the specification, the computer program was reliable.

Workarounds and specification drift: If an error is found but a workaround is used instead of a fix, the workaround effectively updates the specification. If the error recurs because the workaround was not followed, the user is in error — not the software.

Lock mechanisms vs. flexibility: Secure mechanisms prevented astronauts from making errors but also prevented emergency fixes. One such mechanism saved a flight when an interfacing system had an error — a reference to the Apollo 14 incident. The dilemma: “We had not only prevented the astronaut from making any errors, we had prevented him from doing anything.”

Error detection philosophy: “The ‘no-error checking’ philosophy accounted for the majority of recorded system errors.” Early in Apollo, astronauts and users assumed they would know procedures well enough that no checking was needed. They were wrong. But “the more error logic incorporated in the software, the more chance for errors from the additional software.”

Backup system paradox: Backup systems “could not prevent errors any better than the primary system (i.e., generic errors).” Resources spent on backup systems compromised primary system reliability.

The Reject Value

Section titled “The Reject Value”

The paper introduces the AXES specification language and the formal treatment of errors through the Reject distinguished value: a member of every data type. If an input maps to Reject as output, an error has been detected. Functions applied to Reject-containing inputs may propagate or recover.

References

Section titled “References”

1974 Paper

Section titled “1974 Paper”

References include Hamilton’s internal Draper Lab memos, the Apollo flight problem analysis, the “Computer Got Loaded” Datamation letter (reference 4), and related work on structured programming.

1978 Paper

Section titled “1978 Paper”

References include Hamilton’s 1972 analysis of Apollo system problems during flight, the 1976 IEEE TSE HOS paper, and formal methods literature.

Section titled “Related Documents”