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

"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

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