There are only side effects! When you compute a pure function, you’re still physically manipulating registers, cache, etc. You can use the proof-program persp

There are only side effects! When you compute a pure function, you’re still physically manipulating registers, cache, etc. You can use the proof-program perspective to formalize reasoning about a program: - you have some domain model; this expresses the “business logic” of your software - you have an abstract model, in a category for your programming language; this expresses an equivalent structure as the “business logic” - you have a concrete model, in a category for your hardware; this expresses an equivalent structure as it gets executed Reasoning about the translations between these steps, their properties, etc is why you want to connect software to proofs. For example, if you want to find an optimal implementation: you want the shortest path of atomic arrows in your hardware category, which corresponds to the desired computation in your language category. Category theory is the language in which we connect our theory of hardware to our theory of the business domain!