I was speaking with Phil Wadler at ICFP about full-spectrum programming languages, and it came up that Phil wasn’t familiar with the inconsistency in the Sage theorem proving axioms from Knowles et al. ’06. He prodded me to talk about it here.

Here’s the axioms from Knowles et al.’s ’06 Scheme Workshop paper.

The inconsistency is between Faithfulness and Hypothesis. Hypothesis demands that x:{y:Int|false} ⊨ false[y:=x] = false, but Faithfulness requires that x:{y:Int|false} ⊭ false.

Talking with Kenn Knowles, he agreed—Faithfulness should instead say E ⊨ not false—the soundness of the logic comes from not being able to prove false from an empty environment. Kenn had an interesting analysis, which I’m including wholesale:

In practice, of course, the soundness of e.g. SMT is not in question. There are really two important and separable questions that axioms such as those of Ou et al ’04, our Scheme ’06, and our PLPV ’09 conflate somewhat. Neither is answered to my satisfaction.

1. How shall we give semantics to contracts and executable refinement types?

   And the meta-question: Why do so many authors create new and rather different semantics? Perhaps your POPL ’10 and our TOPLAS ’10 may represent a convergence (knock on wood) towards techniques that are both generally effective and simple enough that future work will build upon them rather than just trying to make something simpler, as has happened a few times in the contract space.

   For this question, I feel an axiomatization yields little insight, while a lightweight denotation has a nice explanatory flavor. Thus my perspective is that critiquing axiomatizations does not substantially contribute to this question.

2. How effectively can specifications / proof obligations written in Type Theory or subsets thereof be translated to other logics such as SMT?

   While an axiomatization seems like a way to characterize such translations, the question itself was not the focus of Ou et al ’04, our Scheme ’06, or our PLPV ’09. Without such results the direct and concrete approach of Liquid Types (e.g. PLDI ’08 and ESOP ’13) that simply illustrates a particular mapping may be clearer.

   For this question, I feel an axiomatization falls short unless it has proofs of interesting properties which illuminate why it is a minimal or otherwise “good” set of axioms for characterizing the space of translations/logics. Thus my perspective is that critiquing axiomatizations that already lack such properties/proofs does not substantially contribute to this question.

With regard to Kenn’s first point, Belo et al.’s ’11 syntactic semantics gives one answer for how to give semantics to contracts, though there’s plenty of room for less syntactic analyses.