I am usually programming in Haskell (the little programming I do besides research) and I try to do property based testing a lot. And of course, you have to come

I am usually programming in Haskell (the little programming I do besides research) and I try to do property based testing a lot. And of course, you have to come up with the properties to test for when generating test cases. With a proof doubly so, as you need a specification that you can prove your implementation against. In my time in industry (YMMV) I think I've never seen a formal enough specification that would be useful in that sense. I think we're in a specification crisis where behavior is unspecified and documentation diverges from that as well. APIs break regularily and services are down daily. It's a miracle the whole house of cards has not come down yet.