Talk:Correctness (computer science)
|WikiProject Computer science||(Rated Stub-class, Mid-importance)|
Some sources wanted
Since the term "correctness" is pretty general I suppose there are different definitions for it. Even if I in no way dispute the current one it would be nice with a source so that it would be easy to see where it comes from. Liiiii (talk) 13:58, 20 June 2013 (UTC)
may lie much deeper
Yes, it is bad language but it is also wrong. Proving partial correctness is as difficult as solving the halting problem. I'm not a regular Wikipedia editor, but if there is anyone out there who reads this and cares about accuracy I suggest that you drop that sentence. —Preceding unsigned comment added by 22.214.171.124 (talk) 08:16, 27 August 2009 (UTC)
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)
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.
Hello fellow Wikipedians,
I have just modified one external link on Correctness (computer science). Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
- Added archive https://web.archive.org/web/20160304013345/http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf to http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf
When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.
You may set the
|checked=, on this template, to true or failed to let other editors know you reviewed the change. If you find any errors, please use the tools below to fix them or call an editor by setting
|needhelp= to your help request.
- If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
- If you found an error with any archives or the URLs themselves, you can fix them with this tool.
If you are unable to use these tools, you may set
|needhelp=<your help request> on this template to request help from an experienced user. Please include details about your problem, to help other editors.