The complete specification of the language NASA wrote the Space Shuttle’s flight software in is a 20-megabyte set of page images. There is no text layer. Some pages sit at an angle.
That document is IR-542, and nothing supersedes it. To determine whether a bit-string partition is legal on the left of an assignment, the answer is a photograph of a page printed in 1980.
This is the first of four experiments in what current AI can do with legacy systems, each varying one factor: how degraded is the source of truth, and can the model be caught being wrong. HAL/S is the favourable end. A formal specification exists, real preserved code exists, and an independent implementation exists to check answers against. Establishing what those best-case conditions buy is the reason it is in the study.
The OCR strategy that produces a clean, corrupt result
Run three OCR engines and take the majority. The approach works for prose and fails for grammars.
OCR errors are correlated across engines. Tesseract, Textract and the PDF’s embedded text layer read the same glyphs at the same resolution with similar priors, so they misread ::= the same way and | the same way. A vote between them does not cancel error; it converts three identical mistakes into confident agreement. The deeper constraint is that no aggregation method recovers a candidate no engine produced. If all three miss a character, fusion has nothing to fuse.
For prose this is survivable because context repairs it. For BNF it is fatal: the metacharacters are the content, and no redundancy exists to repair from. Take the vote and the result is a clean, plausible, silently corrupt grammar, with every downstream artifact inheriting the corruption and no symptom to reveal it.
Pages were therefore sorted by how far OCR could be trusted.
| Tier | Content | OCR trust | Disposition |
|---|---|---|---|
| A | Prose | High | OCR, spot-check |
| B | Tables | Medium | OCR plus structural verification |
| C | BNF productions | Low | Hand-transcribe, verify against the scan |
| D | Two-dimensional source notation | Low | Vision model, then verify |
Appendix G — the working grammar, 485 productions across physical pages 295 to 306 — is Tier C throughout. One strong engine produced the authoritative draft. The other two were used to flag disagreement for re-inspection, never as voters. Every production was then read by eye against a zoomed crop of the page image.
Two checks that made verification mechanical
Human attention is the scarce resource, so it is spent only where automation cannot reach. Two checks carry most of the assurance and need no human at all.
Numbering integrity: the 485 production numbers resolve to exactly 1 through 485, with no gaps and no duplicates. The numbers are the specification’s own and the last is 485, which proves nothing was dropped or double-counted across twelve pages.
Reference integrity: every nonterminal appearing on a right-hand side either has a defining production or is one of 22 known lexical primitives. No dangling references, no misspellings.
Between them these catch the entire class of “a page was skipped” and “a name was mangled.” The by-eye pass was then reserved for what the checks cannot see.
One detail shows the value of measuring rather than estimating. A human skim of the PDF reported that some pages sat at an angle, which drove a plan to deskew before OCR. Measurement found skew under 0.3 degrees, and the deskew stage was removed. An estimate was replaced by a number, and the number deleted a stage of the pipeline.
Residual ambiguities were recorded rather than resolved inline: a scaling glyph the scan left uncertain, later settled against the specification’s own prose describing it, and one production logged as an inference from physical scan damage and marked as such.
The implementation
With a verified grammar, the remainder is ordinary compiler work, and the model was strong at it. The result is plain Rust with no cargo and no third-party crates; the crates link in dependency order through a two-stage rustc build.
All twelve preserved Shuttle-era programs run. MATVECS3 puts 22 vector and matrix operations through 400 iterations and reports success. DATATYPES reproduces every value its own comments specify. TEST7 links against a separately compiled COMPOOL and exercises true NAME pointers.
Arithmetic is where fidelity stops being a slogan. SINGLE precision on the Shuttle’s general-purpose computer is IBM System/360 short hexadecimal floating point: it truncates toward zero rather than rounding to nearest, and its precision varies between 21 and 24 bits with the value. IEEE f32 would have been easier and would have produced different numbers. Authentic arithmetic is the default, with a switch to f64 for using the language rather than studying the machine.
Verification against an implementation we did not write
Passing your own tests establishes that the implementation agrees with your understanding, which is the thing under suspicion. Every program is therefore also run through an independent HAL/S interpreter and compared value-for-value. Every program that interpreter can run matches exactly, including all 339 numbers DATATYPES emits. The four it cannot run, this implementation handles.
An independent oracle is a luxury. Two of the other three experiments have none, and the fourth had one deliberately sealed until the work was frozen.
What was left unbuilt
The corpus is closed and so is the scope. Fixed-point scaling, true mid-statement preemption in the real-time executive, the latched and unlatched event distinction, and full 56-bit hexadecimal DOUBLE are unimplemented, each recorded with its reason.
The reason is not difficulty. No preserved program exercises them, so no artifact exists to verify an implementation against. Building unverifiable behaviour is the specific failure this project was structured to avoid, and it is what an eager model will produce on request.
What the favourable case demonstrates
Given a formal specification, real code to test against, and an independent implementation to check answers with, a current model produces a faithful reconstruction of a dead language.
The load-bearing human contributions were narrower than expected, and neither was code review. The first was deciding not to vote between correlated OCR engines — a judgement call separating a good result from a worthless one that looks identical. The second was reading 485 grammar productions against page images by eye, which is bounded by information theory rather than by model capability.
The next experiment removes the specification entirely. The source of truth is a novel, no oracle exists, and one had to be built.