I write code in Agda (a proof assistant) for a living and this is rarely true. Because (1) even if you prove your program is correct as per spec it doesn't prov

I write code in Agda (a proof assistant) for a living and this is rarely true. Because (1) even if you prove your program is correct as per spec it doesn't prove it's correct according to user/PM since spec can/will be buggy (2) proving every single theorem about your system is an extraordinary time sink, an engineer needs to know what parts are higher risk and needs to be proven and which parts are corrolaries of basic algebra and proving is of academic interest. EDIT: In my experience the biggest benefit you get from proof assistants like Coq, Agda etc is being able to run arbitrary unittests within your type system. It's convenient because it makes all bugs a type error and therefore possible to check at compile time. This doesn't mean agda will magically find all bugs, but it means you have more tools to do so.