Talk:Correctness (computer science)

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Computer science (Rated Stub-class, Mid-importance)
WikiProject icon This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Stub-Class article Stub  This article has been rated as Stub-Class on the project's quality scale.
 Mid  This article has been rated as Mid-importance on the project's importance scale.

Some sources wanted[edit]

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[edit]

"may lie much deeper" --> extremely vague grammar —Preceding unsigned comment added by (talk) 21:03, 12 April 2009 (UTC)

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 (talk) 08:16, 27 August 2009 (UTC)

Powerful enough logic[edit]

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[edit]

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

Request redirect[edit]

Can somebody please set up a redirect from Software correctness? — Preceding unsigned comment added by (talk) 19:09, 27 February 2015 (UTC)

External links modified[edit]

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:

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.

Cheers.—InternetArchiveBot (Report bug) 09:49, 13 August 2017 (UTC)