I feel like every time I try to do super formal proofs for code, it ends up way more brutal than I expect and slower than just fixing stuff as I go. Still love types catching my mess-ups for me though.
This is the eternal tradeoff of testing, brought to its logical (no pun intended) conclusion. Testing (and formal verification) don't get you anything for free: writing detailed specs or tests is at least as difficult as writing a correct implementation. In fact given a sufficiently detailed spec, a program conforming to the spec can be derived automatically.
