Re: Looking for new language features (re-elaboration)

genew@shuswap.net (Gene Wirchenko)
21 Sep 2000 18:10:34 -0400

          From comp.compilers

Related articles
[4 earlier articles]
Re: Looking for new language features (re-elaboration) lingolanguage@hotmail.com (William Rayer) (2000-09-13)
Re: Looking for new language features (re-elaboration) brangdon@cix.compulink.co.uk (2000-09-15)
Re: Looking for new language features (re-elaboration) joachim_d@gmx.de (Joachim Durchholz) (2000-09-17)
Re: Looking for new language features (re-elaboration) joachim_d@gmx.de (Joachim Durchholz) (2000-09-17)
Re: Looking for new language features (re-elaboration) vbdis@aol.com (2000-09-17)
Re: Looking for new language features (re-elaboration) Martin.Ward@durham.ac.uk (2000-09-21)
Re: Looking for new language features (re-elaboration) genew@shuswap.net (2000-09-21)
Re: Looking for new language features (re-elaboration) joachim_d@gmx.de (Joachim Durchholz) (2000-09-21)
Re: Looking for new language features (re-elaboration) etoffi@bigfoot.com (2000-09-21)
Re: Looking for new language features (re-elaboration) rhyde@cs.ucr.edu (Randall Hyde) (2000-09-23)
| List of all articles for this month |

From: genew@shuswap.net (Gene Wirchenko)
Newsgroups: comp.compilers
Date: 21 Sep 2000 18:10:34 -0400
Organization: Okanagan Internet Junction
References: 00-08-130 00-09-048 00-09-075 00-09-086 00-09-096 00-09-133
Keywords: design

"Joachim Durchholz" <joachim_d@gmx.de> wrote:


[snip]


>I'd like to see more provision for expressing proofs about program
>properties, and in a way that the "average programmer" can at least
>read and understand.


[snip]


>(I'm aware that there are theoretical and practical problems here, but
>you were asking for ideas, not implementations <g>.)


[snip]


>Regards,
>Joachim
>[I'd like a language that could compile the assertions so I don't have
>to write the code. -John]


          Naughty, naughty!


          I have to say that I am not impressed with the program proof
gang. In one textbook that purported to prove an implementation of
Euclid's Algorithm -- why is this picked so often? -- I found three
errors in the "proven" program.


Sincerely,


Gene Wirchenko


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.