Designing hardware out of category theory
Digital circuits form a category. But what does that really mean? In this talk I’ll present a toy CPU I wrote in category theory. Using FP techniques, the resulting design is type-safe by construction, and polymorphic in its word-size and instruction-set.
Thinking about the distinction between computing on the CPU and computing to build the CPU leads to some interesting perspectives on software. Differentiating between arrows in the category vs arrows in the host language has important ramifications when doing metaprogramming.
Sandy likes improving life and making cool things.