Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!wuarchive!psuvax1!rutgers!cmcl2!sbcs!libserv1.ic.sunysb.edu!jallen
From: jallen@libserv1.ic.sunysb.edu (Joseph Allen)
Newsgroups: comp.lang.misc
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1991Apr13.023921.29746@sbcs.sunysb.edu>
Date: 13 Apr 91 02:39:21 GMT
References: <1755@optima.cs.arizona.edu> <1991Apr11.214018.19443@watmath.waterloo.edu>
Sender: usenet@sbcs.sunysb.edu (Usenet poster)
Organization: State University of New York at Stony Brook
Lines: 24

In article <1991Apr11.214018.19443@watmath.waterloo.edu> mhcoffin@tolstoy.waterloo.edu (Michael Coffin) writes:
>In article <1755@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:

>>[Proofs are equivelent to programs (they had better be).  The only reason
   proofs make programs less buggy is that they add redundancy (it's almost
   as hard to derive the proof as it is to write the program in the first
   place)]

I agree with this completely.

>[Proofs are better because instead of giving detailed steps, they are closer
  in showing that the goals sketched out in the specs are acheived]

If the proofs are detailed enough to detect programming errors than why not
just program in proof-steps (or whatever they're called)?  They are probably
just a "higher" level of abstraction than current programming languages. WE'll
have to make a proof compiler...
--
#define h 23 /* Height */         /* jallen@ic.sunysb.edu (129.49.12.74) */
#define w 79 /* Width */                       /* Amazing */
int i,r,b[]={-w,w,1,-1},d,a[w*h];m(p){a[p]=2;while(d=(p>2*w?!a[p-w-w]?1:0:0)|(
p<w*(h-2)?!a[p+w+w]?2:0:0)|(p%w!=w-2?!a[p+2]?4:0:0)|(p%w!=1?!a[p-2]?8:0:0)){do
i=3&(r=(r*57+1))/d;while(!(d&(1<<i)));a[p+b[i]]=2;m(p+2*b[i]);}}main(){r=time(
0L);m(w+1);for(i=0;i%w?0:printf("\n"),i!=w*h;i++)printf("#\0 "+a[i]);}