All,

Forgive my lack= of deep understanding but I need guidance.

=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0 --

Clearly the statements in Q can be proven using sequent calculus.

But Dijkstra hints at a "Giant Step" kind of reasonin=
g and proof that

enables one to skip the proof of Q, which wo=
uld greatly simplify program

proofs, especially mathematical =
proofs in Axiom.

Consider that, in Axiom, I'm working=
at a proof from both ends. On one

hand I have the code and o=
n the other I have the mathematics.

Sequent logic seems t=
o insist on stepping through every line of the

program. Hoare=
logic seems to imply that it is possible to ignore portions

=
of the program logic provided the Q invariant holds.

Clea=
rly I need to do further study. Can you recommend any papers that

=
might give me more clarity on this subject?

Many tha=
nks,

Tim

David Gries (ed) (= 1978) ISBN 0-387-90329-1=C2=A0 pp80--88

Dear Tim,

--001a113cf5d6e2cfe60552b0fdc0--
From MAILER-DAEMON Sat Jun 24 22:02:51 2017
Received: from list by lists.gnu.org with archive (Exim 4.71)
id 1dOwt0-00051w-Vj
for mharc-axiom-developer@gnu.org; Sat, 24 Jun 2017 22:02:50 -0400
Received: from eggs.gnu.org ([2001:4830:134:3::10]:46827)
by lists.gnu.org with esmtp (Exim 4.71)
(envelope-from ) id 1dOwsy-00051m-Az
for axiom-developer@nongnu.org; Sat, 24 Jun 2017 22:02:50 -0400
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1dOwsw-0008CJ-S0
for axiom-developer@nongnu.org; Sat, 24 Jun 2017 22:02:48 -0400
Received: from mail-wr0-x230.google.com ([2a00:1450:400c:c0c::230]:34795)
by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16)
(Exim 4.71) (envelope-from ) id 1dOwsw-00087c-J2
for axiom-developer@nongnu.org; Sat, 24 Jun 2017 22:02:46 -0400
Received: by mail-wr0-x230.google.com with SMTP id 77so110355066wrb.1
for ; Sat, 24 Jun 2017 19:02:44 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
h=mime-version:in-reply-to:references:from:date:message-id:subject:to
:cc; bh=dxWOm2SjxPt+TmMkwpICkEYJD5eEuD6B6mqxMGddWkE=;
b=AqppeLGTN7EddYI36fe80bsKUyjtRkeS2I+6Xzjwpjjc6AXxibwSapLHgcBxzibAjm
2EsB8RVAVdj9XXX7bg9edL5pbmG8wDOgvBMSsCDV/36TIvNrOSq2vLBJ2NtN33ItDrHm
PM3GulNx+WJFi0ytdCqqLALSemVJJgAJl8deVV065Dqldf7iVnWS7gSUaH97xW7AgIwm
6eaubw779uZY+p5eQ0WBTTyZvjNfvvMk7Brd9XZOmss9sKU6vgDX/VD/PcDC7ljb7OQB
ayGy4cvCgyEV/X7fKC+Xkmiop/9cqR5aCjO4CcpMTtbZzfEFacfDboSOM5F4ekSNmEM/
9amg==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20161025;
h=x-gm-message-state:mime-version:in-reply-to:references:from:date
:message-id:subject:to:cc;
bh=dxWOm2SjxPt+TmMkwpICkEYJD5eEuD6B6mqxMGddWkE=;
b=q6nXvTHn29H4R0EShFTagL1TK1AcfeZ6iKkwi82LI4YmwpfpZVlcK/ha393iuXwsdq
Ol8Gz7KLymTqp+avbirsgNe6f8xubkCQ//sIiB04aG7uGJJgJTi/9axxU3t8cjq2F2nt
waSEwqtBvpaOhEszPq/r/X952TRFhjRgWKLaWtojriHEdOTq/hNsRrykse1A1SlzitwP
Jkc6J+UkKOcZKyWJvkzdSAOUBD//Z3t9HHWYPeMuolnD+9nSY/zFdyo5JwwNHsvhYfoX
Fdv8zhUf+gJkPeZyRPcOeHr2gTlFvjplq+RTVOQuJbwIKzRlgfSgmkzjSmmNEpZO1nNH
pTcQ==
X-Gm-Message-State: AKS2vOwyt1kVWfV23w/pZSe5gYwkZtzPc/ZxzfNbV47cf/DZg8jHLWu9
oOF9DlBqPOk8b/sFsCl62G53oMb3Vw==
X-Received: by 10.223.177.129 with SMTP id q1mr10223566wra.82.1498356163844;
Sat, 24 Jun 2017 19:02:43 -0700 (PDT)
MIME-Version: 1.0
Received: by 10.28.10.142 with HTTP; Sat, 24 Jun 2017 19:02:43 -0700 (PDT)
In-Reply-To:
References:
From: Tim Daly
Date: Sat, 24 Jun 2017 22:02:43 -0400
Message-ID:
To: Jeremy Avigad
Cc: Benjamin Pierce , Klaus Sutner ,
Tim Daly , axiom-dev
Content-Type: multipart/alternative; boundary="f403045e7c7ae4a15a0552bf3a98"
X-detected-operating-system: by eggs.gnu.org: Genre and OS details not
recognized.
X-Received-From: 2a00:1450:400c:c0c::230
Subject: Re: [Axiom-developer] Reconciling Seqents and Hoare Triples
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.21
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Sun, 25 Jun 2017 02:02:50 -0000
--f403045e7c7ae4a15a0552bf3a98
Content-Type: text/plain; charset="UTF-8"
Thanks. Looks like I'll have to deep dive into HOL.
Tim
On Sat, Jun 24, 2017 at 5:03 AM, Jeremy Avigad wrote:
> Dear Tim,
>
> The book *Concrete Semantics*, by Gerwin Klein and Tobias Nipkow, gives a
> nice introduction to reasoning about programs in a proof assistant. It has
> a chapter on Hoare logic. It is available free online:
>
> http://www.concrete-semantics.org/concrete-semantics.pdf
>
> Best wishes,
>
> Jeremy
>
>
>
> On Sat, Jun 24, 2017 at 1:07 AM, Tim Daly wrote:
>
>> All,
>>
>> Forgive my lack of deep understanding but I need guidance.
>>
>> Consider trying to prove a program. The Sequent-style calculus
>> of proofs are of the form:
>>
>> A
>> --
>> B
>>
>> whereas the Hoare triple calculus is of the form
>>
>> A { Q } B
>>
>> Hoare makes the observation that "axioms may provide a simple
>> solution to the problem of leaving certain aspects of the language
>> undefined".
>>
>> Dijkstra [0] observes "This remark is deeper than the primarily
>> suggested applications such as leaving wordlength or precise
>> rounding rules unspecified. Hoare's rules for the repetitive construct
>> rely on the fact that the repeatable statement leaves a relevant
>> relation invariant. As a result, the same macroscopic proof is
>> applicable to two different programs that only differ in the form of
>> the repeatable statements S1 and S2, provided that both S1 and S2
>> leave the relation invariant (and ensure progress in the same direction).
>>
>> Clearly the statements in Q can be proven using sequent calculus.
>> But Dijkstra hints at a "Giant Step" kind of reasoning and proof that
>> enables one to skip the proof of Q, which would greatly simplify program
>> proofs, especially mathematical proofs in Axiom.
>>
>> Consider that, in Axiom, I'm working at a proof from both ends. On one
>> hand I have the code and on the other I have the mathematics.
>>
>> Sequent logic seems to insist on stepping through every line of the
>> program. Hoare logic seems to imply that it is possible to ignore portions
>> of the program logic provided the Q invariant holds.
>>
>> Clearly I need to do further study. Can you recommend any papers that
>> might give me more clarity on this subject?
>>
>> Many thanks,
>> Tim
>>
>> [0] Dijkstra, Edsger W. "Correctness Concerns and, among Other Things,
>> Why They Are Resented" in Programming Methodology Springer-Verlag
>> David Gries (ed) (1978) ISBN 0-387-90329-1 pp80--88
>>
>
>
--f403045e7c7ae4a15a0552bf3a98
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Tim

--f403045e7c7ae4a15a0552bf3a98--

The book *Concrete Semantics*=
, by Gerwin Klein and Tobias Nipkow, gives a nice introduction to reasoning=
about programs in a proof assistant. It has a chapter on Hoare logic. It i=
s available free online:

Best wis=
hes,

Jeremy

On Sat, Jun 24=
, 2017 at 1:07 AM, Tim Daly <axiomcas@gmail.com> wrote:

=

=

leave the relation invariant (and ensure progress in th= e same direction).the repeatable statements S1 and S2, provided that both= S1 and S2applicable to two different programs that only differ in t= he form ofrelation invariant. As a result, the same macroscopic p= roof is rely on the fact that the repeatable statement leaves = a relevantrounding rules unspecified. Hoare's rules for the repetitiv= e constructsuggested applications such as leaving wordlength or preci= seDijkstra [0] observes "This remark is deeper than the pr= imarilyundefined".=solution to the p= roblem of leaving certain aspects of the languageHoare makes the ob= servation that "axioms may provide a simple=C2=A0=C2=A0=C2=A0 A { Q } Bwhereas the Hoare triple calculus is of the for= m=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0 B=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0 Aof proofs are of the form:All,Consider trying to prove a program. The Sequent-style calculus=

Forgive my lack of deep understanding but I need guidance.<= br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 --Clearly the statements in Q can be pro= ven using sequent calculus.But Dijkstra hints at a "Gia= nt Step" kind of reasoning and proof thatenables one to= skip the proof of Q, which would greatly simplify programpr= oofs, especially mathematical proofs in Axiom.Consider t= hat, in Axiom, I'm working at a proof from both ends. On one<= div>hand I have the code and on the other I have the mathematics.Sequent logic seems to insist on stepping through every line of th= eprogram. Hoare logic seems to imply that it is possible to = ignore portionsof the program logic provided the Q invariant= holds.Clearly I need to do further study. Can you recom= mend any papers thatmight give me more clarity on this subje= ct?Many thanks,TimWhy They Are Resented" in Programming Methodology Springe= r-Verlag

[0] Dijkstra, Edsger W. "Correctness Concerns and, among Other Thin= gs,

David Gries (ed) (1978) ISBN 0-387-90329-1=C2=A0 pp80--88

Thanks. Looks like I'll have to deep dive in=
to HOL.

On Sat, Jun 24, 2017 at 5:03 AM, Jeremy Avigad =
<a=
vigad@cmu.edu> wrote:

Dear Tim,The book *Concrete Semantics*, by = Gerwin Klein and Tobias Nipkow, gives a nice introduction to reasoning abou= t programs in a proof assistant. It has a chapter on Hoare logic. It is ava= ilable free online:=Best wishes,Jeremy

<= /div>On Sat, Jun 24, 2017 at 1:= 07 AM, Tim Daly <axiomcas@gmail.com> wrote:leave the relation invariant (and ensure progress in the same directi= on).the repeatable statements S1 and S2, provided that both S1 and S2relation invariant. As a result, the same macroscopic proof isrely on the fact that the repeatable statement leaves a relevantro= unding rules unspecified. Hoare's rules for the repetitive construct= Dijkstra [0] observes "This remark is deeper than the primarilyundefined".solution to the problem of leav= ing certain aspects of the languageHoare makes the observation that= "axioms may provide a simplewhereas the Hoare triple calculus is of the form=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 B==C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 AAll,=of= proofs are of the form:

Forgive my lack of deep understanding but I need guidance.

Consider trying to prove a program. The Sequent-style calculus

= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 --

=C2=A0=C2=A0=C2=A0 A { Q } B

suggested applications such as leaving wordlength or precise

=

applicable to two different programs that only differ in the form of

=

=Clearly the statements in Q can be proven using sequ= ent calculus.But Dijkstra hints at a "Giant Step" = kind of reasoning and proof thatenables one to skip the proo= f of Q, which would greatly simplify programproofs, especial= ly mathematical proofs in Axiom.Consider that, in Axiom,= I'm working at a proof from both ends. On onehand I hav= e the code and on the other I have the mathematics.Seque= nt logic seems to insist on stepping through every line of theprogram. Hoare logic seems to imply that it is possible to ignore portion= s of the program logic provided the Q invariant holds.Clearly I need to do further study. Can you recommend any paper= s thatmight give me more clarity on this subject?W= hy They Are Resented" in Programming Methodology Springer-VerlagMany thanks,Tim[0] Dijkstr= a, Edsger W. "Correctness Concerns and, among Other Things,

Da= vid Gries (ed) (1978) ISBN 0-387-90329-1=C2=A0 pp80--88