The group you are posting to is a Usenet group. Messages posted to this group will make your email address visible to anyone on the Internet.
Your reply message has not been sent.
Your post was successful
 |
Newsgroups: comp.software-eng
From: run...@hpirs.HP.COM (Mark Runyan)
Date: 24 Jan 90 22:26:42 GMT
Local: Wed, Jan 24 1990 5:26 pm
Subject: Re: Have *YOU* ever written a program which COULDN'T be proven correct?
I hate stepping in sticky piles of whatever...
>>I've been trying to follow this string, remembering those days in college Note the term I used, "proof of correctness"... >>when the instructor indicated that program proof of correctness ... >Indeed, I doubt *ANYONE* on the entire net has *EVER* written a There is a difference (perhaps only in *my* mind) between using the >real-life program which couldn't in theory be verified. We all (well, >except for a few of those who posted earlier) know that finding a >decision procedure for the predicate calculus (called the >"Entscheidungsproblem" and "Hilbert's Program" in various places) is >impossible, and therefore the halting problem and program verification >are undecidable. predicate calculus proof of correctness and program verification. If we call code inspections and regression testing "proofs", then, I do prove my programs. I was under the mistaken expression that someone was using an automated proof assistant. My apologies to netters for stepping into an argument where I didn't share the same understanding of the terms. Mark Runyan You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
| |||||||||||||