“Computational functions are reflected, at the logical level, as pairs of a precondition and postcondition. […] A function’s precondition and postcondition alone determine how it is lifted: its code is ignored. (The conformance of a function’s body to its declared pre- and postcondition
is checked, of course, via a proof obligation […]) This reflects a philosophy in which the only way of reasoning about the behavior of a function value is via its specification: code never appears within formulae.” — It seems that it took a very long time until this extremely natural idea was finally incorporated in a decent Hoare logic for functional programs (and a couple more years until it finally reached the world of refinement type systems 😉 )
“In this paper, we […] allow specifications to be expressed in higher-order logic. The intuitive justification for this approach is that, if functions can abstract over functions, then specifications must abstract over specifications.”
- Yann Régis-Gianas and François Pottier. A Hoare logic for call-by-value functional programs. In Proceedings of the Ninth International Conference on Mathematics of Program Construction (MPC’08), pages 305-335, July 2008.