patternMinor
Why proving programs correctness doesn't have the same importance as algorithms analysis or the theory of computation in practice?
Viewed 0 times
provingwhythesamecomputationtheoryimportanceanalysiscorrectnesspractice
Problem
What are the major causes that makes "Proving Programs correct", not a widely attractive subject? though from it's name, and from what we know from other disciplines (like mathematics) it looks like it should be on the top of the "must know list". And by the way I'm talking about "the real world", in practice.
Solution
On the contrary, it's certainly important practice, and is a huge area of research!
Perhaps a better question might be, "why is proving programs correct not common in practice, or not a main feature of an undergraduate curriculum?"
There's a few reasons for this:
Things also change by what you mean by a "program". For example, in real world algorithms research, almost every time someone publishes a new algorithm, they will provide a proof of correctness. Usually this is working on pseudocode with a simple but straightforward semantics, so lots of the formal details from above aren't an issue.
Also, just to counter your claim that it's not an area of research:
Perhaps a better question might be, "why is proving programs correct not common in practice, or not a main feature of an undergraduate curriculum?"
There's a few reasons for this:
- Proving programs correct is hard. The proofs often end up being long and tedious proof-by-cases, and will usually have less interesting intellectual content that you'd see in most math proofs.
- You need a formal semantics for whatever language your program is specified in. For real world programming languages, developing such a semantics is often difficult, since there are possibly corner cases or odd compiler behaviors that are difficult to model
- Proving a program correct only proves that it matches a given specification. What if there's a bug in the specification?
- Proving a program correct assumes that it's being compiled by a correct compiler, or run by a correct interpreter, which almost never the case.
Things also change by what you mean by a "program". For example, in real world algorithms research, almost every time someone publishes a new algorithm, they will provide a proof of correctness. Usually this is working on pseudocode with a simple but straightforward semantics, so lots of the formal details from above aren't an issue.
Also, just to counter your claim that it's not an area of research:
- The entire field of Dependent Types is focused on proving real, running programs correct using type theory. There are lots of great projects in this area, like DeepSpec.
- Formal methods is an entire field devoted to proving program correct, usually adapting methods from hardware verification to software.
Context
StackExchange Computer Science Q#68484, answer score: 9
Revisions (0)
No revisions yet.