Field notes · 5 June 2026
The bridges nobody had built
A factory that builds in Ada eventually walks into a plain wall: the language can talk to C, but somebody has to write the bridge first — and for several libraries we wanted, nobody had. So we wrote them. Then we gave them away.
Ada is the language we build in. It is how we make software whose correctness can be proven rather than hoped for. But real programs don’t live in a vacuum — they draw graphics, load images, read a camera, put a panel on a screen. Across the whole industry those jobs are done by a handful of well-worn C libraries. To call one of them from Ada you need a binding: a thin, careful layer that lets the two languages talk without either side getting confused about memory or types.
For the libraries we reached for, the Ada package ecosystem had a gap where the binding should be. Vulkan — the modern graphics and compute API — had no Ada binding at all. Rather than abandon the plan, or write the bridge privately and keep it to ourselves, we built four and published them, open-source:
| Crate | What it binds | Repository |
|---|---|---|
vulkan_ada |
The Vulkan graphics & compute API — with a SPARK-proven safety layer | the-dark-factory/vulkan-ada |
ccv_ada |
Liu Liu’s CCV computer-vision library | the-dark-factory/ccv-ada |
stb_ada |
Sean Barrett’s STB libraries — image load / write, TrueType | the-dark-factory/stb-ada |
imgui_ada |
Dear ImGui, the immediate-mode GUI toolkit | the-dark-factory/imgui-ada |
What these are — and what they are not
Here is the honest part, and it matters to us more than the libraries do. Three of these four are bindings, and nothing more. A binding is a bridge to someone else’s C; it does not — cannot — prove that C correct. We did not verify CCV’s computer vision, or STB’s image loader, or Dear ImGui’s widgets. They are other people’s work, and good work; our part is the careful bridge, not a proof of what is on the far side of it. Calling them “verified” would be a lie, so we don’t — and you won’t find them in the verified-conversion tally the rest of this site is so particular about.
A binding is not a proof. We won’t pretend otherwise.
There is one exception, and it earns its own paragraph. vulkan_ada carries a small layer of SPARK contracts on top of the raw binding, and that layer is proven. It turns the classic ways of misusing a graphics resource — using a handle after you have destroyed it, building a child object from a parent that is already gone — into mistakes the compiler refuses to build, rather than crashes you discover at runtime. We are not aware of another Vulkan binding, in any language, that carries a machine-checked safety layer like it. The binding underneath is still just a binding; the safety layer on top is the proven part, and we are careful to say which is which.
Why give them away
We have written before that a factory inverts the old economics — that when you can manufacture a component on demand, a borrowed dependency stops being a win and becomes a liability. That is still true. But a binding is the one kind of thing where the logic runs the other way. It isn’t a moat; it is a bridge to a library that everyone already shares. There is nothing in it to own, and no reason for the next person who wants to call Vulkan from Ada to build the same bridge from scratch.
So we put them where they belong: in the open, under permissive licences, in the the-dark-factory organisation, for anyone to use. If they save one other person a week of fiddly C-to-Ada plumbing, they have done their job.
And if you would like the things you couldn’t afford to build properly to suddenly fit — come and talk to us.