-
alifib, the language of higher-dimensional diagrams
alifib is an experimental programming language and interactive proof assistant in which programs are diagrams — not illustrations of programs, but the syntax itself, the internal representation, and the thing that is checked and run.
-
SDCPNs: A Common Language for Complex Systems
Formal guarantees of AI safety begin as a modelling problem: to reason rigorously about whether an AI-controlled system is safe, you first need a mathematical representation of that system. This post builds a Stochastic Dynamic Coloured Petri Net up from an ordinary Petri net, one feature at a time, and then uses three cyber-physical examples — an industrial gas supply chain, a truck fleet, and a semiconductor fab — to show the range of systems the resulting formalism can represent.
-
Changing the frame: formal modeling with LLM assistance
Every formal model — a scientific model, an engineering design, a program, a spreadsheet — is expressed within some frame that fixes the concepts available and the rules the expression must obey. Computing has overwhelmingly preferred unconstrained frames, and LLM assistance is making the resulting drift of abstractions worse. This post argues for frames that are more constrained but can be changed fluidly, and works through a case study in structured spreadsheets: inferring a schema for a flight-itinerary dataset, tightening it with types and path equations, and then restructuring it.
-
Why Supply Chains Are an Ideal Testbed for Safeguarded AI
Supply chains pair interrelated decisions with high-consequence outcomes, which is what makes them an ideal proving ground for Safeguarded AI — a world model that predicts an action’s consequences, an explicit specification of acceptable outcomes, and a verifier that can establish the system satisfies it.