Types as axioms, or: playing god with static types | Heykuki News