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.
“This principle Try to imagine someone wanting to learn something about your code while reading as little of it as possible, which I didn’t even know existed, is now one of the things I think about every time we change the language.”
“A new way to play NES Tetris has recently been discovered, and it’s leading to new world records.”
“The punk movement is anti-establishment, with long ties to political activism and resistance, anti-consumerist, anti-corporate, anti-authoritarian, with a strong ethic of visibility and in-your-face active expression of these sentiments. Punk is also messy. While the grimdark hero, forged by a traumatic backstory and strewing trails of corpses through the sunless waste, is one opposite of the Disney Princess, hopepunk is another opposite.”
“Sensory science can therefore be seen as a form of creative production, as it tries to locate flavours at scale in replicable and reliable ways”
“Yet if I had to pick one policy that was the Platonic ideal of stupid, the thing that has almost zero upside and also has the best ratio of 'amount of damage this is doing to America’ versus ‘reasons why we can’t stop being idiots about this’ there is (so far) a clear winner.”
See also: verilog2factorio
“Everyone knows this coffee shop is owned by loan sharks. It’s probably a money laundering operation”
OpenMower - The affordable Open Source DIY Smart GPS Robotic Mower
“Put in another way: turning all the German nuclear reactors back on could approximately stop gas imports from Russia. Shutting the remaining ones down could increase the dependency on Russian gas by about 30%. So why doesn’t Germany do it?”
“From race science to the noble savage, the history of anthropology is cluttered with the corpses of convenient stories, of narratives that misrepresent human diversity to advance ideological aims. Is primitive communism any different?”
“Welcome to the inside story of the MIT Banana Lounge.”