> It's precisely because most developers are terrible at mathematical reasoning that so much software is so difficult to reason about -- there are tons of unnec

> It's precisely because most developers are terrible at mathematical reasoning that so much software is so difficult to reason about -- there are tons of unnecessary special cases, when hidden inside all the tangled logic there's secretly a simple set of axioms and theorems that lend themselves to intuitive composition. Have you ever developed software outside of academia? Special cases arise when your perfect mathematically structured snowflake is put in the hands of actual users who want to do actual work with it. A buddy of mine who did work with JPL has told me that NASA uses a decades-old FORTRAN app to calculate orbits. When I asked him why they didn't port it to a more modern language he said it was because the system has so many special cases and fudges that would take forever and the new system might not be able to replicate the features of the old one. Of course having a logical basic architecture (example, a structure that encodes special cases as configuration) can make it easier to maintain as a project matures.