Diff — AdaLog

{{infobox

| title = AdaLog

| subject = A Prolog-style logic engine written in Ada 2012 with SPARK formal-verification annotations — designed to give game characters a reasoning brain

| span = TitaniumComplete-0.2 era → AdaLog v0.9, TitaniumWM v2.2, TitaniumRun v0.4, TitaniumBG v0.7

| author = Rocky L. Oliver — the workshop that would later build AdaLogic BASIC

| status = Unreleased open source — BSD-3-Clause license bundled with the TitaniumWM release

| the idea = What if a game's AI could *prove* its options instead of just scoring them — one solver step per frame, no heap, no surprises

| related = [[Vector Symbolic Architectures]] · [[Reversible Computing]] · [[Year of the Linux Desktop]]

| image = ada-lovelace.jpg

| caption = Ada Lovelace (1835 portrait). Her namesake language hosts both the Titanium suite and AdaLogic BASIC — two languages, one lineage.

}}

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.[[cite: TitaniumComplete-0.2 source tree — AdaLog v0.9, TitaniumWM v2.2, TitaniumRun v0.4, TitaniumBG v0.7; the suite's bundled license is BSD-3-Clause, copyright 2026 Rocky L. Oliver.]]

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 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 [[Year of the Linux Desktop|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).[[cite: AdaLog main.adb — the test harness prints "Titanium Engine: Utility AI Test", identifying the logic engine as the suite's namesake core.]]

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

```text

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.

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.[[cite: types.ads — Atom_Base 1_000_000, Var_Base 2_000_000, and the fixed pool sizes that bound the whole engine's memory.]]

- **`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`.

[[File:adalog-orc.svg|right|340px|The orc's decision, drawn from my main.adb: facts and rules flow into the stepped solver, which enumerates every proven option; the caller takes the argmax.]]

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*:

```text

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.[[cite: titanium_logic.ads — Unify's Post aspect: a failed unify restores Env and the trail pointer; backtracking via Trail_Array.]]

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.**

```fact

Why the solver steps.

A normal Prolog runs to exhaustion. I made AdaLog's solver resumable instead: Initialize, then Step → Running/Found/Done, yielding after each solution. That's not a limitation — it's the design. A game loop can budget inference per frame, take one solution, render, and resume next tick. The logic engine cooperates with the frame rate instead of fighting it.

```

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*.[[cite: main.adb — the utility-AI demo: see/health facts, attack/heal rules, stepped solving, argmax decision; output ends "Chosen Action: heal, Final Score: 500".]]

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.

[[File:ti-tiling.svg|right|340px|TitaniumWM's tiled layout: a master area beside a stack column, 12 workspaces, all keyboard-driven.]]

[[File:getac-titaniumwm-xterm-split-panes-01.jpg|right|340px|TitaniumWM live — xterm split panes and the color-coded tab bar, running on the [[Getac B300-X]]. Photograph by Rocky L. Oliver.]]

[[File:getac-titaniumwm-firewall-firefox-tabs.jpg|right|340px|Firefox tiled under TitaniumWM — real desktop, real workload. Photograph by Rocky L. Oliver.]]

**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.[[cite: TitaniumWM README and src/main.adb, layout.ads — SPARK_Mode On for layout/state; the X11 event loop is explicitly non-SPARK by design.]]

**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.[[cite: TitaniumRun src/completion.ads, launcher_core.ads — Max_Candidates 8192, Max_Results 5, Pre/Post contracts on every buffer operation.]]

[[File:ti-desert.svg|right|340px|The desert_mountain scene, schematized: a buzzard cycles through its state machine over the dunes while the coyote holds its scripted coordinates.]]

[[File:getac-pixel-art-desert-wallpaper-01.jpg|right|340px|desert_mountain rendered live — the buzzard mid-flight over the dunes, on the B300's sunlight-readable display. Photograph by Rocky L. Oliver.]]

**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.[[cite: TitaniumBG src/desert_mountain.ads, titanium_bg.ads — Buzzard_State machine, Wallpaper_Item tagged type, Pixel_Array bounded to 3840×2160.]]

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.

[[File:ada-lovelace.jpg|right|240px|Ada Lovelace — the namesake. The suite sits in a lineage that runs from her notes on Babbage's engine to SPARK formal verification.]]

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.

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.

- [ ] 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.

```hide Show answers — click to check yourself

1. **True** — facts, rules, unification, a trail for backtracking: a deliberately small, provable Prolog.

2. **True** — `Post => (if not Success then Env = Env'Old and T_Ptr = T_Ptr'Old)` in titanium_logic.ads.

3. **False** — it's stepped on purpose (`Step` → Running/Found/Done) so a game loop can budget inference per frame.

4. **True** — `Buzzard_State` cycles Circling → Descending → Feasting → Ascending in desert_mountain.ads.

5. **False** — the suite is unreleased open source (BSD-3-Clause bundled), a personal workshop — which is exactly the point.

```

- 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.

- The live-capture photographs (TitaniumWM panes, Firefox tab, the desert wallpaper) were taken on the author's [[Getac B300-X]] — the same machine the suite was largely written on.

- 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.

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.

[[Category:AdaLogic BASIC]]

[[Category:Languages]]

[[Category:Programming]]