Talk:Correctness
From Wikipedia, the free encyclopedia
[edit] Powerful enough logic
Hmm - doesn't the bit about Curry-Howard depend a bit on which constructive logic? At the lower levels, you just get some sort of type-checking ... --Charles Matthews 15:51, 18 Apr 2004 (UTC)
- Well, strictly speaking it's true at "lower levels" as well, it's just not so interesting. Simple type checking is a form of correctness, though.
- But I accept your point that for a logic to be expressive enough to represent the normal notions of correctness it should probably at least have predicates/dependent types.
- This should properly be discussed in the main CH-iso article, or even better, one on program extraction. How about we just add a "suitably expressive" qualifier here, and some discussion of correctness versus type-checking? --Eoghan 20:36, 19 Apr 2004 (UTC)
-
- Well, yes - that's why I raised it. I did a first CH article; I've seen some grumbling about it. If people really take it that CH reaches as far as some sort of proof unwinding, or Martin-Lof type theory, or something of that strength, then there should be some way of expressing that, over there. --Charles Matthews 21:15, 19 Apr 2004 (UTC)
[edit] Program proving systems
There have been a number of reasonably successful program proving systems, and they should be discussed. These include, at least
- The Stanford Pascal Verifier (late 1970s)
- The Pascal-F Verifier (early 1980s)
- The DEC Modula verifier (early 1990s)
- ESC, Extended Static Checking for Java (late 1990s)
- The Microsoft Spec# effort. (mid 2000s.)
All of these are based on the Nelson-Oppen complete decision procedure approach. That whole line of work needs to be discussed. All of the systems listed can be found in Google.
Program proving probably should be under "program verification" (currently a stub) and some of the content from "formal verification" should be moved there. Then, "correctness" and "formal verification" can be merged. I'll start on this in March if no one objects.
--John Nagle
