The Curry-Howard correspondence would like a word. Any time you write a program, you are also writing a proof.
Mechanized proof checkers leverage this idea to enable users to specify formal proofs as programs.
Mechanized proof checkers leverage this idea to enable users to specify formal proofs as programs.
In practice, writing programs and finding proofs feel like quite different activities, and at least in my experience of doing both I almost never try to write a program by thinking "how could I prove that such-and-such a type is nonempty" and I literally never try to prove something by finding a corresponding type and writing a program that computes or represents something of that type.
The Curry-Howard isomorphism is a beautiful theorem, and as you say it inspires some nice methods of automated proving / proof-checking, but I don't think it says anything much about the relationship between the programming and theorem-proving activities that actual humans engage in.
True, and (mostly) irrelevant. When I write a program, I am also writing a proof, but I don't care about it as a proof. It proves something that I am completely uninterested in proving. But as a program, it's a program that I am interested in running.
Interesting that you contradict yourself in successive sentences
By running the program, you, in fact, demonstrate that you are quite interested in proving whatever it is you wrote
No, I didn't. You managed to either completely miss my point, or to completely ignore it.
Just in case you didn't ignore it, let me try again. I could care about a proof for the sake of the proof. If that were the case, I probably wouldn't write a program, I'd just write the proof. (Yes, that could be mechanically turned into a program, but I didn't actually do that, because I cared about the proof rather than the program.)
When I write a program, I usually care about it as a program, not as a proof. When I write a GUI, say, I care about how it enables the users to access the rest of the program's features. You can turn that into a proof, and the compiler may in fact do so, but what it proves is something that is really unrelated to what I'm trying to do. The "proof" won't prove anything about usability or human factors or pleasing color scheme or user workflow or efficient use of screen real estate. It will prove something that, from the programming point of view, is completely uninteresting.
So, as I said, I'm not interested in the proof, I'm interested in the program. And, despite the correspondence, they are not the same thing.
Maybe not in the abstract - but you are, in fact, "interested in the proof": because when the program doesn't do what you want it to, you either have to fix it so it does prove your use case, or you've proven that what you were trying to do was incorrect
A function List -> Sorted List can both be considered a proof that lists can be sorted as well as a procedure for sorting lists.
Edit: And for this topic in question, If you don't understand what you are proving then you aren't working with proofs. I really doubt that programmers actually constructs their programs by mapping it to mathematical statements, seeing what it proves and then mapping it back to a program, so they are writing programs, not proofs.