AdaLog

Before there was AdaLogic BASIC, I wrote AdaLog — and before there was a language to document, there was a workshop's worth of software quietly proving the thesis that would later drive ALB: that Ada is the right metal to build serious things on, and that programs should be able to prove what they do.

AdaLog is a Prolog-style logic engine I wrote in Ada 2012 with SPARK annotations, built as a utility-AI brain for games — a tiny reasoning machine that stores facts and rules, unifies them, and hands back provable answers one step at a time. It shipped with a small desktop suite I built around it at the same time: TitaniumWM, a SPARK-annotated tiling window manager for X11; TitaniumRun, a dmenu-style launcher; and TitaniumBG, a procedural animated-wallpaper renderer with its own state machines.^[1]

None of it was ever released. All of it survives, source and binaries intact — a complete snapshot of my software workshop in the years before ALB.

The Titanium workshop

The suite shares more than a name. Every program I wrote in that period is in Ada, every core module carries pragma SPARK_Mode (On), every data structure is statically bounded — no heap, no malloc, no allocation after startup — and every piece was built to be understood, in the tradition of the hand-built desktops of the window-manager underground.

The naming runs deeper than branding. AdaLog's own test program announces itself as --- Titanium Engine: Utility AI Test --- — the logic engine was the Titanium Engine. The suite and the language were one project with four faces: a brain (AdaLog), a desktop to run it on (TitaniumWM), a way to launch things (TitaniumRun), and something worth looking at while I thought (TitaniumBG).^[2]

What AdaLog actually is

Strip the name away and what's left is a genuine logic-programming kernel — a deliberately small, deliberately provable descendant of Prolog:

see(orc, player).
health(orc, 15).

score(orc, attack, 100) :- see(orc, player).
score(orc, heal, 500)  :- health(orc, H), H < 20.

Facts declare the world. Rules derive scores from it. A query — score(orc, Action, Points). — asks the engine to find every action and its score, and the caller picks the best. That is the entire interface between a game and its character's judgement.

The design target I had in mind was unusual and specific: utility AI for games. Most game AI scores options imperatively — an if ladder, a behavior tree, a hand-rolled scorer. I wanted to know: what if the scoring were logical? A rule only fires when its conditions are provably true against the world state; the engine doesn't just rank actions, it derives them. An orc doesn't get a "heal" score because a programmer wrote if hp < 20 then heal — it gets one because health(orc, 15) unified with health(orc, H), bound H = 15, and the sub-goal H < 20 was proven. The decision carries its own proof.

Anatomy of a tiny Prolog

The whole engine is eight Ada units, each small enough to read in one sitting — and each doing exactly the job its name claims:

• Types — the value system. Every term is a Term_ID (a plain integer); atoms intern from 1,000,000 upward, variables from 2,000,000 upward, leaving small integers free to be literal numbers — the reason health(orc, 15) and H < 20 can mix names and arithmetic in one fact. All bounds are constants I picked deliberately: 2,048 atoms, 64 variables, 1,024 facts, 256 rules, a 256-entry trail, up to 3 arguments per fact and 16 sub-goals per rule.^[3]
• Atoms — the intern table, mapping names like score and orc to their IDs and back.
• Titanium_Lexer / Titanium_Parser — text to tokens to goals. The parser is what turns score(orc, Action, Points). into a machine-usable query.
• Titanium_Database — the fact base and rule store: Assert_Fact, Assert_Rule, static pools, SPARK Abstract_State.
• Titanium_Logic — the heart: the Environment (variable-to-term bindings), the Trail (the undo log that lets the engine take back every binding it ever made), Deref, Unify, and Backtrack.
• Titanium_Solver — the driver: Initialize a query, then call Step repeatedly; each step reports Running, Found, or Done.

The SPARK difference

Any competent programmer can write a Prolog in a weekend. What I cared about in AdaLog is that its unification isn't just correct — it's contracted:

procedure Unify (T1, T2 : Term_ID;
                 Env   : in out Environment;
                 Trail : in out Trail_Array;
                 T_Ptr : in out Trail_Index;
                 Success : out Boolean)
  with Post => (if not Success then Env = Env'Old
                                  and T_Ptr = T_Ptr'Old);

Read the postcondition aloud: if unification fails, the environment and trail pointer are provably unchanged. A failed match can never leave half-written bindings behind to poison the next attempt — not because I reviewed the code, but because the contract states it and SPARK can prove it. That single line is the difference between a logic engine that probably works and one whose failure behavior is a theorem.^[4]

The same discipline runs through everything I built in the suite. Titanium_Database exposes Abstract_State rather than globals; TitaniumRun's launcher buffer carries Pre/Post contracts (Insert_Char requires room, Backspace requires content); TitaniumWM's Layout package is pure logic — Tile_Windows takes screen dimensions and computes positions, provably separated from the X11 event machinery that calls it. The whole suite is built on one pattern: bounded static state, contract-checked behavior, pure logic at the core, impure I/O pushed to the edges.

The orc test

AdaLog's demo program is the whole pitch in 150 lines of Ada. It interns the atoms, asserts a two-fact world — the orc sees the player, and the orc has 15 hit points — asserts two scoring rules, then runs the query score(orc, Action, Points). one Step at a time.

The solver's first Found is attack at 100 points — the orc sees you, so attacking is provable. The second Found is heal at 500 — health(orc, H) unifies, H binds to 15, 15 < 20 proves, and the wounded orc's self-preservation outscores its aggression. Done ends enumeration, and the harness takes the argmax: the orc heals.^[5]

It is a small thing — a toy world, two rules — but it demonstrates the complete claim: a game character whose possible actions are derived from provable facts about its situation, enumerated exhaustively, and selected by score. Behavior trees can imitate this; AdaLog can prove it.

The desktop trio

TitaniumWM (v2.2) is the flagship of the trio — a hybrid tiling window manager I wrote for X11, in the tradition of dwm and its kin but in Ada 2012. All three desktop tools were built and tested on FreeBSD — releases 12 and 14 — as well as Linux; they were, from the start, a BSD desktop environment as much as a Linux one. Master-plus-stack tiling and full-screen monocle, twelve persistent workspaces, color-coded window decorations for focus state, everything driven from the Alt key — and, critically, a design split stated plainly in the code: the layout and state logic is SPARK-annotated while the X11 boundary is not (pragma SPARK_Mode (Off) sits honestly atop the event loop, because X event marshalling is a C world). The stated goal is "minimal memory footprint with no heap allocation after initialization" — a window manager you could, in principle, verify.^[6]

TitaniumRun (v0.4) is the launcher — the same idea as dmenu or rofi: type, complete, run. Its Completion package keeps a fixed table of 8,192 candidate names (truncated at 16 characters), returns at most 5 matches, and annotates every buffer operation with contracts. A program whose entire job is to fuzzy-match a string carries formal proof annotations about that string's length. That is the Titanium sensibility in miniature — and honestly, it's the part of the suite I'm most amused by.^[7]

TitaniumBG (v0.7) is the surprise — an animated procedural wallpaper engine. Each scene is a tagged object with Render and Update methods, drawn into a bounded pixel buffer sized for up to 4K displays. The desert_mountain scene keeps a coyote at fixed scene coordinates (220, 210) and runs a buzzard through a four-state machine — Circling → Descending → Feasting → Ascending — on its own RNG seed and frame counter. Jungle river, plasma fields, a snowy village round out the set, drawn by a hand-rolled VGPU layer with its own ditherer and fonts. It's a desktop wallpaper that thinks — and like the WM and launcher, it runs clean on FreeBSD 12 and 14.^[8]

Why Ada, of all languages

To the rest of the world, building a logic engine, a window manager, and a wallpaper renderer in Ada is eccentric. To me it was the obvious choice — Ada is the language industry already trusts where failure isn't an option: avionics, rail, medical. SPARK is its proof subset, where contracts aren't comments but checkable claims. The bet behind the whole suite — and behind ALB after it — is that the same discipline belongs on the desktop, in the game loop, in the wallpaper, and eventually in the language toolchain itself.

And there is a fittingness to it: a language named for the first person to write about programming as a discipline — Lovelace's notes on the Analytical Engine argued the machine could manipulate symbols according to rules, not merely calculate — hosting a system whose entire purpose is symbol manipulation by rule. Prolog's dream, Ada's rigor, one workshop.

The road to ALB

AdaLog answers a question ALB's existence raises: why would anyone build a language? Because I'd already built one. The Titanium suite is the evidence — I wrote a Prolog engine when I needed game AI, a window manager when I wanted a desktop, a renderer when I wanted wallpaper. ALB is what happened when the same instinct aimed at the language itself.

The pattern carried over intact: static bounds instead of dynamic allocation, contracts instead of conventions, a compiler pipeline of small honest units — lexer, parser, logic, solver, the same nouns that now structure albt.adb's tokenizer, parser, and emitters. AdaLog v0.9 was the rehearsal. AdaLogic BASIC is the production.

Quiz

• AdaLog is a logic-programming engine in the Prolog family, written in Ada with SPARK annotations.
• Its Unify procedure carries a formal postcondition: failed unification provably leaves the environment unchanged.
• AdaLog's solver runs to completion in one call and cannot be interrupted.
• TitaniumBG's desert scene includes a buzzard that cycles through behavioral states.
• The suite was a commercial release competing with mainstream desktop tools.

Notes

• This article is written in the first person — the software is the author's own, and the account is primary testimony rather than secondhand reporting.
• All technical claims trace to the TitaniumComplete-0.2 source tree itself — the suite is unreleased, so the code is the documentation. Version numbers are the bundled ones: AdaLog v0.9, TitaniumWM v2.2, TitaniumRun v0.4, TitaniumBG v0.7.
• Screenshots of the running TitaniumWM and TitaniumBG are forthcoming and will join the schematic figures in this article.
• Licensing: TitaniumWM's release bundles a BSD-3-Clause license (© 2026 Rocky L. Oliver); the suite has also been described as Apache-2.0. Both are permissive — the material fact is that the code is open and unshipped.
• The SPARK boundary is reported honestly: core logic packages carry SPARK_Mode (On); the X11-facing event loop in TitaniumWM's main.adb is explicitly SPARK_Mode (Off). "SPARK-annotated" is the accurate claim, not "fully verified."
• FreeBSD compatibility: TitaniumWM, TitaniumRun and TitaniumBG were all built and tested on FreeBSD 12 and 14 — a 100% working BSD desktop trio, not merely portable-in-principle.
• The orc demo's "Chosen Action: heal, Score: 500" is the program's actual designed output — a wounded orc that can see you heals rather than attacks, because the rule set scores it so.

References

1. AdaLog-v0.9/AdaLog/ — atoms, titanium_lexer, titanium_parser, titanium_logic, titanium_solver, titanium_database, types, main (Utility AI test), TitaniumComplete-0.2.
2. titanium_logic.ads — Unify contract and trail-based backtracking.
3. types.ads — Term_ID ranges, atom/variable interning scheme, static pool bounds.
4. TitaniumWM-v2.2/ — src/main.adb, layout.ads, wm_state, wm_keys, x11; release README and BSD-3-Clause LICENSE.md.
5. TitaniumRun-v0.4/ — src/completion.ads, launcher_core.ads.
6. TitaniumBG-v0.7/ — src/desert_mountain.ads, jungle_river, plasma, snowy_village, titanium_bg.ads, vgpu renderer/ditherer/fonts.
7. Ada Lovelace, notes on the Analytical Engine (1843) — the symbolic-manipulation lineage.