I just formalised a key part of geometric dimensioning and tolerancing (GD&T) which is the standard language used by engineers for communicating how much a manufactured part is allowed to vary from its original, intended design.

Repo: https://github.com/OliverP255/formal-gdt