Comment by mafribe

I wonder if we are talking about the same things. Do you use Hoare logic or interactive proof assistants when putting "nto practice formal proofs of correctness", and find that that lowers your software engineering costs? I would be surprised if that was the case.