6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ It's too difficult, too expensive, and too time-consuming (for the average programmer and software project). So in short, it's not worth it. $\endgroup$ – Juho Jan 10 '17 at 13:56
9
$\begingroup$

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:

  • 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.
$\endgroup$
  • $\begingroup$ thank's, that's what i meant: "why is proving programs correct not common in practice, or not a main feature of an undergraduate curriculum?" $\endgroup$ – Maykel Jakson Jan 9 '17 at 21:20
  • $\begingroup$ Dijkstra famously championed an approach to teaching CS that was based on formal proofs: On the cruelty of really teaching computing science, also the Wikipedia article $\endgroup$ – adrianN Jan 10 '17 at 8:39
  • $\begingroup$ One interpreter that we rarely think about is the CPU hardware itself, which interprets machine instructions. We usually assume it to be bug-free, but while that may have been true of the earliest devices, it's certainly not the case now: danluu.com/cpu-bugs $\endgroup$ – j_random_hacker Jan 10 '17 at 15:25
  • $\begingroup$ @j_random_hacker There definitely are bugs, but formal verification is used much more heavily in hardware design than in software, at least as I understand it. $\endgroup$ – jmite Jan 10 '17 at 17:59
  • $\begingroup$ one other yuuge problem you did not mention: it's useless for interactivity. it'd great where you have genuine functional routines, but that only covers part of the spectrum of real world programming. $\endgroup$ – user48832 Jan 11 '17 at 20:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.