You are making a categorical error: One proves algorithms and tests programs.
You can prove programs too, not just algorithms. That's what the entire (exorbitantly expensive) field of verified applications lies upon. Even my college class on formal logic covered the basics of this, and there's billions of dollars worth of extremely high-reliability applications that have been developed using such formal proofs.
For example, Green Hills Software's INTEGRITY operating system has bounds on the runtime and behavior of system calls formally verified, so one can reasonably guarantee that a malicious user cannot DDOS the system by making system calls with unbounded duration.
There are even entire programming languages designed for the sole purpose of making formal, mathematical verification of programs easier.
A program is a representation of an algorithm.
Yes, which is why you have to prove it correct again, since real programming languages, e.g. C, have limitations not typically present in the original algorithm.
The programs that can be proven are severely limited in power. For one, the tools to prove correctness of programs can't deal with data other than integers[1].
The way this usually works is that the proof is written and the code is then generated from the proof. That code is then incorporated in something larger, which has not been proven correct. Such is the case with algorithms. You can mathematically prove an algorithm correct. You can even write a proof and generate a program from it. Then you still have to use that algorithm and all the code using it can't be proven correct with current methods. That is why you will still have to test your program.
There are even entire programming languages designed for
the sole purpose of making formal, mathematical
verification of programs easier.
Yes, and their practical usefulness is still severely limited.
[1] Of course, in theory this means they can deal with any data; in practice it means they can't.
For one, the tools to prove correctness of programs can't deal with data other than integers.
This is the first time I hear such claim. Which tools are you talking about? The tools I know (Coq) certainly don't have such limitations -- why would they, anyway?
For performance reasons. The SPIN model checker, which is the state of the art in terms of performance, employs only integers.
Has Coq ever been used to solve an actual practical industrial or business problem, either by generating code from a known correct program or by using the Coq model as an oracle to drive automatic testing? If not, then there's your answer: academically useful proof assistants cannot deal with real world data. Proof assistants useful in the real world can only deal with limited data types to be able to achieve their goal.
you can prove theoretical programs. do you really want to have to prove that it still works with any random bit flipped at runtime? what about two random flipped bits?
All proofs start from some assumptions. When you are proving programs, you assume that the hardware is functioning properly. After all, anyone going to the expense of proving their software is correct will also pay for ECC throughout their hardware. Once you've proven your software correct, you can make assurances about the behavior of the software when run on particular hardware, and those assurances will be limited primarily by the reliability of the hardware.
You're challenging what it means for something to be a proof, which I think is always subject to philosophical debate. Intuitively, something is a proof of a proposition if it convinces someone else that the proposition is true, and the proposition actually is true.
Obviously, for difficult concepts, it's possible that every expert in the world could be convinced that a proposed proof is correct, only to later find out that it's not. The way I see it, you're always only proving that something has a high probability of being correct, and showing how high the probability is. For computer software, you might be showing that your program is correct with the same probability that the underlying hardware is working as specified (so cosmic rays shifting bits or faulty hardware are possible exceptions baked into your proof).
To get a bit silly, a mathematical proof delivered from person A to person B is really only showing that a proposition is true with the same probability that person B is sane, educated, and is understanding the concepts correctly,
You can prove programs too, not just algorithms. That's what the entire (exorbitantly expensive) field of verified applications lies upon. Even my college class on formal logic covered the basics of this, and there's billions of dollars worth of extremely high-reliability applications that have been developed using such formal proofs.
For example, Green Hills Software's INTEGRITY operating system has bounds on the runtime and behavior of system calls formally verified, so one can reasonably guarantee that a malicious user cannot DDOS the system by making system calls with unbounded duration.
There are even entire programming languages designed for the sole purpose of making formal, mathematical verification of programs easier.
A program is a representation of an algorithm.
Yes, which is why you have to prove it correct again, since real programming languages, e.g. C, have limitations not typically present in the original algorithm.