Reynolds is stated as the inventor of parametricity. But it seems to me that the same idea is stated quite clearly by Dijkstra in 1970 in this note: https://vanemden.wordpress.com/2018/10/29/history-of-structured-programming/#EWD288
In addition, Dijkstra broaches the interesting idea that proofs ought to be constructed at the level of the flowchart first. Once that is done, using high level steps, it can be refined into code. But the proof of the code is essentially a refinement of the proof of the flowchart. This idea is interesting in that it is often the case that a flowchart might say "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 easier to prove than a low-level inductive proof of a program loop that implements the search and involving issues such as finding invariants. To my mind, this "hierarchical proof technique" (my words, not Dijkstra's) is rather interesting. Tim
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
