Post

1/3 Proving very basic properties of software can have huge impacts. The NASA Mars Climate Orbiter failed due to a mismatch between Pound-seconds (Imperial) and Newton-seconds (Metric). This mistake cost $327 Million.

gavin.codes

@gavin.codes

2/3 Theorems which use dimensional analysis are absolutely trivial to prove and can be discharged 100% of the time as they fall into decidable theory: linear algebra. We can adorn python with units and get iron-clad assurance of correctness with no runtime cost and no additional code.

4/6/26, 8:33 am0 reposts0 likes

gavin.codes

@gavin.codes

4 June

3/3 Axiomander, our MCP for proving properties of python, shows how easy it is to augment python with this capability. Why isn't everyone already doing this?