Your reply message has not been sent.
Your post was successful
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 collegeNote 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 aThere 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
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.
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.