🚀 go-pugleaf

In article <25711@cup.portal.com> mmm@cup.portal.com (Mark Robert Thorson) writes:
>There was an excellent article about 10 years ago in CACM on this.
>I believe the title was "The Social Process and Proofs of Program
>Correctness".  This article marked the death of program verification;

I must've missed the boat: I always prove my programs correct.  Pathologies
in provability (which are theoretically guaranteed) almost always indicate
flaws in design.  Therefore undecibeability is actually an AID in program
verification, not an obstacle.

Programs in even languages like C, Pascal can be manipulated via a set of
(complete) algebraic rules -- which form a foundation for the semantics
of the language in question.  I use such rules all the time.

>... from that point on the "conventional wisdom" was that program
>verification was a dead-end for research.  In retrospect, it's hard
>hard to see why this wasn't obvious from the very beginning.

Oh, the irony...