Talk:Correctness (computer science)

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

"may lie much deeper" --> extremely vague grammar —Preceding unsigned comment added by 18.202.1.175 (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 130.238.11.75 (talk) 08:16, 27 August 2009 (UTC)

Actually, proving total correctness would require solving the halting problem. I have just fixed the vague wording--better late than never. -- UKoch (talk) 14:52, 26 June 2020 (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.

--John Nagle

Request redirect

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

External links modified

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.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• 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.

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