axiom-developer is up and has been for year=
s.

Reynolds is stated as the inventor o=
f parametricity. But it seems to me that the

same idea is stated q=
uite clearly by Dijkstra in 1970 in this note:http= s://vanemden.wordpress.com/2018/10/29/history-of-structured-programming/#EW= D288

In addition, Dijkstra broache=
s the interesting idea that proofs ought to be constructed

at the=
level of the flowchart first. Once that is done, using high level steps, i=
t can be

refined into code. But the proof of the code is essentia=
lly a refinement of the proof of

the flowchart. This idea is inte=
resting in that it is often the case that a flowchart might

say &=
quot;find the largest value such that...", which when reduced to code =
would involve a loop.

A proof that the largest value exists at th=
e abstract "flowchart" level would be easier

to prove t=
han a low-level inductive proof of a program loop that implements the searc=
h

and involving issues such as finding invariants.

=

To my mind, this "hierarchical proof technique" (m=
y words, not Dijkstra's) is rather

interesting.

Tim

I don't see where parametricity is stated in this note=
; you'll have to be more

parametricity theorem: every function in the polymorphic lambda calculus=

specific.

Reynold=
s credits Christopher Strachey for distinguishing ad hoc

and para=
metric polymorphism.=C2=A0 What Reynolds realized and proved is the

(and a few other type constructors) is parametric.=C2=A0 Giving =
a technical

formulation of this (related values of related types =
are mapped to related

results) is a major advance in our understa=
nding of how to reason about

programming languages as a whole and=
individual programs, too.=C2=A0 Among

other things, data abstrac=
tion (a concept Reynolds certainly did not invent)

is a consequen=
ce of the parametricity theorem.

=C2=A0 - Frank

On Wed, Nov 7, 201=
8 at 2:54 PM Tim Daly <axiomcas@gm=
ail.com> wrote:

Reynolds is stated as the inventor of parametric= ity. But it seems to me that thesame idea is stated quite clearly= by Dijkstra in 1970 in this note:

https://vanemden.wordpress.com/2018/10/29/history-of-structured-programmi= ng/#EWD288In addition, Dijkstra b= roaches the interesting idea that proofs ought to be constructed= at the level of the flowchart first. Once that is done, using high level st= eps, it can berefined into code. But the proof of the code is es= sentially a refinement of the proof ofthe flowchart. This idea i= s interesting in that it is often the case that a flowchart mightsay "find the largest value such that...", which when reduced to= code would involve a loop.A proof that the largest value exists= at the abstract "flowchart" level would be easierto p= rove than a low-level inductive proof of a program loop that implements the= searchand involving issues such as finding invariants.To my mind, this "hierarchical proof technique&qu= ot; (my words, not Dijkstra's) is ratherinteresting. Tim

Frank Pfenning, Profes=
sor

Computer Science Department

Carnegie Mellon Uni=
versity

Pittsburgh, PA 15213-3891

+1 412 268-6343

GHC 6017

All,

<= /div>

This paper about ISA Semantics for ARMv8-A, RISC-V, a=
nd CHERI-MIPS

https://alastairreid.github.io/papers/popl19-isasemantics.p= df

https://alastairreid.github.io/papers/popl19-isasemantics.p= df

is interesting. It seems to provide a "base case"=
; for proving programs

correct. In particular, they seem to be ab=
le to generate proof code for

various provers, including Coq.

One of the criticisms about "proven program=
s" is that they tend to

ignore implementation details. But g=
iven a lisp variant, Milaw, that

is proven to the hardware instru=
ctions this new step is really important.

A proof =
of the machine instructions, a proof of milawa on top of those

in=
structions, a proof of lisp extensions on top of milawa, and a proof

<=
div>of Axiom's spad language on top of lisp turns into a fully validate=
dtower.

It appears that all of this (an=
d it is an impressive pile) can be developed

in Coq.

Also of interest, while I was part of the CMU CERT effort=
I developed

the ISA for the Intel 32 bit processor [0]. My progr=
am reads Intel binary

and generates "Conditional-Concurrent =
Assignment" semantics. I may

be able to re-target the back e=
nd to their Sail language which would

provide ISA semantics for I=
ntel 32 in Coq.

Tim

[=
0]

Daly, Timothy<= span class=3D"gmail-T21"> Intel Instruction Semantics = Generator SEI/CERT Research Report, Mar= ch 2012

&g=
t; John writes:

> This "only" proves down to the=
binary API. Is there proven hardware?

Their effor=
t is only "proven to binary" but they do manage to run Linux on i=
t.

There is a language called Verilog to speci=
fy "down to the wires and transistors"

See htt=
ps://www.utdallas.edu/~gxm112130/papers/iscas15.pdfThere is "Project Oberon" which is designing a =
"complete desktop computer from

scratch" staring f=
rom the wires and transistors. Their lowest layer is in Verilog on

http://www.projectoberon.com/

I have an Altera Cyclone FPGA that can run their RISC-V Verilog

The pr=
oof game at this level involve mealy/moore state machines since

e=
verything happens all at once on real hardware.

but haven't yet had=
the time to run the Oberon code.

So eventually th=
e Coq proof runs from FPGA <-> Binary <-> Jitawa <->

Milawa <-> ACL2 / lisp <-> Axiom spad <-> algorithm=
spec <-> Coq proof.

It will take longer than I expect but =
all of the parts are there.

On Sun, Nov 11, 2018 at 7:09 PM Tim Daly <axiomcas@gmail.com> wrote:

All,= This paper about ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS

https://alastairreid.github.io/papers/popl19-isasemantics.pdfvarious provers, including Coq.One of the criticisms about "proven programs&qu= ot; is that they tend toignore implementation details. But given= a lisp variant, Milaw, thatis proven to the hardware instructio= ns this new step is really important.A proof of t= he machine instructions, a proof of milawa on top of thoseinstru= ctions, a proof of lisp extensions on top of milawa, and a proof= of Axiom's spad language on top of lisp turns into a fully validated=tower.It appears that all of this (and it= is an impressive pile) can be developedin Coq.<= br>Also of interest, while I was part of the CMU CERT effort I d= evelopedthe ISA for the Intel 32 bit processor [0]. My program r= eads Intel binaryand generates "Conditional-Concurrent Assi= gnment" semantics. I maybe able to re-target the back end t= o their Sail language which wouldprovide ISA semantics for Intel= 32 in Coq.Tim[0] <= br>Daly, Timothy Intel Instruction Semantics Generator SEI/CERT Research Report, March 2012