← Back to Kevin's newslettersPublished: 2022 May 31

Ever since I first came across ‘em, I’ve been fascinated by the promise of SMT solvers: Just state your problem, and the computer will find you a solution. They’re the epitome of computer as mysterious genie, sometimes granting immense power, other times punishing one’s impertinence by delivering exactly what was asked for.

(Alloy, which I explored back in 2018, leans into this dynamic; the whole tool is oriented around generating concrete instances of abstract specifications to help you realize all of the constraints you inevitably take for granted and leave unsaid.)

I’ve always wanted to apply SMT solvers on a real-world problem — something more than toy logic puzzles (Sudoku as “hello world”) or numeric optimizations (Feb 2021 newsletter).

Last summer, I finally came across a problem rich enough to explore both the conceptual (problem-formulation) and logistical (data input/output) capabilities of SMT solvers. I used the Z3 SMT solver to build a microcontroller search tool and through autumn refined the ideas into a programming language of sorts, informed by the needs of my various microcontroller-based projects.

While the specific context of my exploration is embedded programming, the motivation has always been much more general: To learn to leverage SMT solvers. So even if you care nothing about microcontrollers or pins, you might still enjoy the writeup as a window into an alternative programming universe.

Misc. stuff