Hello, World

Every programmer's first program prints two words into the void and waits to see if anything answers back. Consider this ours.

I'm Chukwuma Akunyili, and this is the first word from Invariant Software — a consultancy I started in Lagos, Nigeria, on a stubborn conviction: that software can be correct on purpose, not correct by luck.

Why "invariant"

In computer science, an invariant is a property guaranteed to hold no matter what the rest of the system does — a contract the program promises never to break. A binary search keeps its target within shrinking bounds. A balanced tree never tips over. The promise holds at every step, under every input, for the life of the program.

I named the company after that word because it is the standard I want to be held to. Most software doesn't fail because the problem was hard; it fails because the system allowed a state that should never have existed. Our job is to make those states impossible — not to catch them later, but to ensure they can never be born.

The two things software owes your machine

I fell in love with two languages, for two different reasons. Between them, they name what this company stands for.

OCaml taught me correctness. Edsger Dijkstra warned us decades ago that "program testing can be used to show the presence of bugs, but never to show their absence." Tests tell you where you are; they can't tell you where you can never go — but types and proofs can. In the lineage that runs through Gérard Huet's work at INRIA, a program and a proof are two faces of the same object: to construct the program correctly is to prove the theorem. And as Yaron Minsky put it at Jane Street — "make illegal states unrepresentable." If your data model can express a broken state, your code will eventually construct one. So we design types where the bug simply will not compile.

C++ taught me performance. It taught me to respect the machine — that every abstraction has a price, that someone somewhere pays for the cycles and the bytes, and that caring what the computer actually does is not premature optimization but professional respect.

These two values pull against each other, and I won't pretend otherwise. The safest code is not always the fastest; the fastest code is often where correctness goes to die. The craft is holding both in tension and being honest — for your problem — about where the line belongs. We reach for OCaml where correctness matters most, and we go closer to the metal when performance is the requirement that pays the bills.

We don't just say it — we ship it

A value you only print on a homepage is decoration. So here is the proof.

Our first product, Chaufr, models a ride as a state machine in OCaml. A ride cannot be completed unless it was first accepted; it cannot be accepted twice. Not because we wrote a test that checks for it — because the types will not allow such a value to exist. The illegal state is unrepresentable. Minsky's principle isn't a poster on our wall; it's the shape of the code.

The thing it owes people

Correctness and performance are what our software owes your machine. But software is built by — and for — people, and a shop that ships correct, fast systems while being slippery to deal with still fails the people who hired it. So our third commitment is about conduct, not code: candor. We give you the honest assessment — of your system, your options, and our own limits — even when the honest answer is "you don't need us for this." Correctness, in the end, is also a way of treating people.

In the open

I believe in free and open-source software — not as a slogan, but as how serious work gets done and how trust gets earned. So we will build in the open, write about the decisions as we make them, and let the work speak before the pitch does.

In three lines

• Correctness — the bug that can't be written.
• Performance — respect for the machine.
• Candor — the truth, even when it costs us the work.

Hello

That's us. If you're building something that has to be right — or something fast that still has to be right — I'd like to hear about it.

Talent can come from anywhere. Let's build something that lasts.

— Chukwuma