Go work for someone like Rockwell Collins doing avionics software. Mostly what they do is test, test, test, and at the end of a long day of testing, they test some more. I know, because some of my best buddies scored jobs there, and now they do Ada in front of green screens.

I suppose that's one way to make a living.

Proving programs correct most probably sucks for anything non-trivial. What are you going to prove? That it follows the specs? Broken as designed would devolve to "proven worthless". So it comes back to writing good specs. Good bedside material.

Finally, don't sell metaphors short ... metaphors are a well tested mechanism for transmitting knowledge between human beings.