ACAS flies again.

Vincent Coen has kept a real accounting system in the open since 1976. Here it is, brought back to the web.

Convert my code → Have a system like this? We’ll do the same for yours.

In 1976 Vincent Coen started writing an accounting system. He is still maintaining it. Across fifty years, through CP/I and CP/M and CIS COBOL and GnuCOBOL, ACAS — the Applewood Computers Accounting System — kept its books, and Vincent kept it in the open for anyone to read — fifty years aloft and never once losing altitude. There is almost nothing else like it.

We took ACAS as a test subject for our formal-verification tooling. To be exact about what that means: the prover runs on our Ada, not on Vincent's COBOL — you cannot point gnatprove at COBOL. What we pointed at his system was a differential oracle, which drives both versions over the same inputs and compares ours against what his actually printed. It held up on every item we tested, to the exact day. That is not the result those tools usually give. So rather than write about it, we did the thing that seemed more fitting: we put it back on the web, running, free, with his name on it.

The man who kept it alive

• By dayTeaches pilots to fly the Boeing 737
• By craftA programmer par excellence — fifty years and counting
• ACASAuthor since 1976; CIS COBOL conversion 1983, for Applewood Computers
• AndStrangely, genuinely, liked COBOL — and it shows in the code

A man who teaches others to fly airliners and, for the pleasure of it, keeps a fifty-year-old ledger honest in a language the world declared dead three times over. When we told him his own code agreed with a machine proof on every case we checked, he was not surprised. He had told us, from memory, that it would.

The same decision, twelve ways

Here is what tells you Vincent built this well. We took that ageing decision and wrote it out in a dozen different languages — from the COBOL he typed in the seventies to a single line of SQL — and ran every one of them over the same set of debts. They all agree. Every language, every item, the exact same column:

Muddled logic does not survive that journey — it drifts, it disagrees, it falls apart in the retelling.

His does not. A decision clean enough to say identically in twelve tongues was a decision made clearly in the first place, fifty years ago, by someone who knew exactly what he meant. That is the smart part, and it is his.

How to use it

ACAS is a terminal program from before the web — no mouse, no windows, and Vincent is the first to say it is not glamorous. But it is not hard, and most of it runs in batch: you tell it a date, it does the work, it prints. Here is enough to find your way around.

The live menu

When you open the live system you get three choices — press the number, no Enter needed:

• 1Run the aged debtor report — drives Vincent’s real sl120 and prints who owes what, sorted by how overdue it is.
• 2The two-cycle reconciliation — posts payments, closes a period, and shows the balances rolling forward exactly as they should.
• 3The proof beside the original — builds the machine-checked Ada and compares it to the COBOL, item by item, live.

Reading the report

The aged debtor report is a list of customers and, for each, how much they owe you split by how late it is. That split is the whole point of the thing — it tells a business who to chase. Each amount lands in one of five columns:

A customer in credit — where you owe them — is shown as Cr Bal and always sits in Current, however old: a credit is not an overdue debt. That is one of the quirks the machine proof preserves exactly, rather than “tidying” away. At the foot of the report the Account Statistics block totals it all, and a Reconciliation block shows the period’s movement — balance brought forward, invoices posted, payments taken, carried out.

If a date is asked for

Some steps ask for a date — type it as DD/MM/YYYY (Vincent is British; the day comes first) and press Enter. Everything else is a yes/no or a single key. There is nothing you can break: the live system runs on a fixed demonstration ledger and resets itself, so poke at it freely.

What we did to bring it back

None of this touched Vincent’s source. Every step below runs his own code, unmodified; where our version differs from his, we treat that as a finding to report to him, never a silent “improvement.” Here, plainly, is the work.

1. Got the source running at all. ACAS uses indexed (ISAM) files, and modern off-the-shelf GnuCOBOL ships without a backend that can compile them — every file handler fails. So we built GnuCOBOL 3.2 against a real Berkeley DB, in a clean container, and the tree came to life: 264 of its 275 programs compile, the main menu among them.
2. Drove his programs through their own doors. We wrote a small rig that creates a test ledger by calling ACAS’s own file handlers (acas012, acas019) — the same doors every ACAS program uses — then runs his unmodified sl120 against it. The rig is ours and clearly marked never-to-be-mixed with his code.
3. Made it deterministic. Run it twice and the report is byte-for-byte identical; run it in a fresh machine and it is identical again. No clock, no randomness leaks in. That repeatability is what lets anyone else check our claims.
4. Re-expressed the heart of it as proven Ada. We took the ageing decision — which column each debt falls into — and wrote it in SPARK Ada, then had a theorem prover (gnatprove) check it: no overflow, no divide-by-zero, and the classification correct against its own specification, for all inputs, not just the ones we tried.
5. Held the two side by side. We ran his COBOL and our proven Ada over the same ledger and compared them item by item — twelve aged invoices, a credit note, payments, and six cases sitting exactly on the 30/60/90-day boundaries, where a rewrite is most likely to drift. They agreed on every one. Twenty-one out of twenty-one.
6. Proved the method is not language-bound. We rendered the same logic into Java and ran it over the identical cases — it agreed too. Faithful in COBOL, in proven Ada, and in Java: the original, the proof, and a third language, all landing every debt in the same column.
7. Put it on the web. Wrapped his real system in a browser terminal so anyone can open it and run it, and rendered the ageing logic into the JavaScript running on this page, so the proof executes in front of you.

One honest boundary: the machine proof so far covers the ageing decision, not yet every line of the program. The faithfulness — that our versions do what his does — is shown for everything the rig exercises; the proof is being extended program by program, in the open, with his behaviour as the reference throughout.

Try it yourself

There is a browser console listing every program in ACAS — all ten systems, taken from Vincent’s own menu source — which will read a folder of ACAS data on your own machine and never uploads any of it. It is honest about what it can and cannot do: no ACAS program has been compiled to WebAssembly yet, and the console says so per program rather than pretending.

Open the ACAS console → Instructions are on that page, below the console.

The results

We have finished a first differential pass over sl120: its decisions rebuilt as proven Ada packages, then driven over the same fixture and compared against the figures Vincent’s own program printed. That produced findings in his code, and it produced three occasions where we were wrong and had to withdraw a claim — one of which he caught himself.

None of it is published here yet, and that is deliberate. The standing agreement is that every finding goes to Vincent first, with the fixtures that produce it and the time to deal with it his own way. He has the full report and has been asked whether we may publish it, in whole, exactly as a paying customer would receive it — including the parts where we were wrong. Until he answers, this section stays as it is.

When it goes up it will carry the coverage gaps beside the results rather than in an appendix, because a report that only shows what it reached is not worth reading.

Why bother

Because fifty years of one person’s careful work deserves to be more than a dormant archive. Because a system that survives a theorem prover unbowed is worth showing people. And because the best thing you can do with something built with that much care is let it keep working — free, in the open, for as long as anyone wants to look.