Two conversions. One we finished, one we never will.
Everybody has an impossible customer — the one who never pays on time and whose job never ends. Ours is a dead operating system from 1965. We are going to start with that one, because what a firm cannot do tells you more than what it can — and because how it behaves on the job that will never pay tells you how it behaves on yours.
The two studies below are chosen to sit against each other. One system has a living author who answers the phone, source that still compiles, and output we can hold our work against. The other has none of those things. That single difference — whether an oracle exists — decides almost everything about whether a conversion is tractable, and it is worth more than any amount of talk about tooling.
Multics, and why we will never finish it
We have been converting Multics modules to SPARK Ada in public for months. The line runs continuously. It is good at what it does. And it will not finish, and we would rather say so here than let a growing number on a dashboard imply otherwise.
Here is the state of a re-classification running over a pinned snapshot of 219 modules, of which 84 are done:
| Class | Count | Meaning |
|---|---|---|
| Proven | 2 | Contracts present and every obligation discharged. |
| Memory-safe only | 3 | Runtime checks all discharged, no functional contract. |
| Partial | 32 | Contracts written, obligations outstanding. |
| Unproved | 43 | Runtime checks undischarged. Nothing is yet proved. |
| Vacuous | 4 | Discharged for a reason that proves nothing. Counted against us. |
Across those 84 modules, 6,469 runtime checks were analysed and 1,528 remain undischarged — 24%. Modules compile at around 96%. Compiling is not proving, and the gap between those two figures is the honest subject of this study.
Why it cannot be finished
There is no oracle. This is the whole of it. Multics has no users, no running instance we can drive, and no printed output to hold a conversion against. We can prove the Ada does not overflow or run off an array. We cannot show it does what the PL/I did, because there is nothing left to ask.
Scale, and the shape of the remaining work. Every module needs contracts a person has to reason about. Machines are good at the transcription and poor at deciding what a forty-year-old subroutine was actually promising. That does not scale by adding hardware.
And the honest commercial answer: nobody is paying for it and nobody will. It is a research corpus that happens to be historically important, and it earns its keep by breaking our tools in ways a paying customer's code must not.
So why is it here?
Because it is the clearest statement we can make about how far we are prepared to go.
We have kept the hardest conversion anybody could name running continuously, for months, for a customer who does not exist and will never pay. We publish the count of what is actually proven — two — rather than the count of what merely compiles, which is around ninety-six per cent and would look far better on a slide. And when our own instruments flattered us, we said so in public: two corrections on that page are against ourselves, a checker that under-read failures, and a label wrongly awarded to 92 modules that had not earned it.
Nobody made us do any of that. There is no client to disappoint and no contract to breach. It is simply the standard, and the reason for showing it here is straightforward: this is the treatment your system would get. If we will spend months on a dead operating system and then publish the two figures that make us look worst, you can reasonably guess how we would report on a system somebody depends on.
The full scoreboard, corrections and all →ACAS, and the man still maintaining it
ACAS is the Applewood Computers Accounting System. Vincent B. Coen began writing it in 1976
and has never stopped; the copyright line reads 1976–, with nothing after the
dash. He is 79 and answers the phone from one o'clock.
Everything Multics lacks, ACAS has. The source compiles. The programs run. And crucially the original prints things — a 132-column report whose every figure can be held against a conversion. That makes the original its own specification, and correctness becomes a question with an answer: does our version agree with his?
So the method inverts. Rather than proving Ada against a document, we pin the original, rebuild its decisions as small proven packages, and compare against what his program actually printed — with the inputs and the expected values coming from two independent files so that nothing is circular.
What it produced
A first differential pass over sl120, the aged debtors report: its decisions
rebuilt as proven Ada and compared line by line against Vincent's own output. It found things in
his code. It also produced three occasions where we were wrong and had to withdraw a
claim — one of which he caught before we did.
The results are not published here yet, deliberately. Our standing agreement with Vincent is that every finding reaches him first, with the fixtures that produce it and the time to handle it his own way. He now has the full report and has been asked whether we may publish it in whole — including the parts where we were wrong. Until he answers, this section stays as it is.
What the pair is meant to show
Not that we are clever. Two proven modules out of eighty-four is not a boast, and three withdrawn claims in one engagement is not a sales pitch.
What it shows is the thing worth knowing before anyone hands over a system they cannot afford to break: ask whether an oracle exists. If your original still runs and still prints, a conversion can be checked against it, and every disagreement can be found and ruled on before anything ships. If it does not, no amount of proof will tell you the new one behaves like the old one, and any vendor who says otherwise is selling you the easier problem.