Why Higher-Order Logic Is a Good Foundation for Deep Verification — Sequent BlogInteractive theorem provers let us make unusually strong claims about software: instead of testing selected executions or trusting a solver&rsquo;s verdict, we state a property mathematically and construct a proof checked by a small logical kernel. That baseline leaves a foundational choice — which logic should the prover implement?<br>The dominant modern answer is some form of dependent type theory, as found in Lean and Rocq. Dependent type theories are strictly more expressive at the type level than the simple type theory underlying HOL4 and HOL Light: they can encode facts about data directly into its type and unify programs and proofs in one language.<br>At Sequent we use HOL4 — not because dependent types cannot support serious verification (they plainly can), but because classical higher-order logic occupies a particularly effective point in the design space for deep verification: proving high-level, application-specific properties all the way down to the machine code that executes. The central question is not which foundation can express the most. It is where each foundation puts complexity, and how much of that complexity must be trusted.<br>Expressive Enough, but Deliberately No More<br>Higher-order logic combines simple types with functions and predicates as first-class objects. That is enough to describe everything that arises in a software stack: language syntax and semantics, transition systems and execution traces, compilers and compiler-correctness relations, program logics, instruction sets and machine states, nondeterministic environments and adversarial programs. It can quantify over predicates, relations, functions, and programs, and it supports induction, recursive definitions, algebraic datatypes, quotients, and conventional classical mathematics. In practice, it is difficult to identify an end-to-end software-verification theorem whose statement genuinely requires types that depend on values.<br>This matters because type-level expressiveness is not free. In a dependent type theory, dependency becomes part of type checking itself: the trusted checker may have to account for dependent products, universes, inductive families, recursors, and a rich notion of definitional equality. HOL takes a more restrained position — use types to rule out basic category errors, and use propositions to state semantic facts. That restraint is a limitation. The question is whether it is a useful one.<br>Should Correctness Be in the Type?<br>The standard showcase for dependent types is the length-indexed vector: a function can state in its type that appending vectors of lengths m and n returns one of length m + n. More ambitious encodings represent only well-typed programs, only balanced trees, or only states satisfying a protocol invariant — &ldquo;making invalid states unrepresentable.&rdquo; Where an invariant is stable, canonical, and preserved by every operation, this is an excellent interface.<br>But many properties in system verification do not have that shape. A byte sequence from an untrusted source may be valid under one protocol version and invalid under another; one parser may accept it while another rejects it; its validity may depend on configuration or prior state, and we may need to reason about what happens when it is malformed. There is no single type that captures what the object is — only multiple contextual facts that may hold about it. The same is true throughout a verification chain: a machine state satisfies several independent invariants, a target program is related to a source program under a particular compiler relation, a trace satisfies a safety property while violating a liveness condition. These facts overlap, evolve, and belong to different abstraction layers.<br>Predicates preserve that independence:<br>well_formed format bytes<br>compiler_related source target<br>state_invariant environment state<br>safe_trace program trace<br>The carrier object stays stable while the properties, contexts, and proof techniques vary. An intrinsic encoding, by contrast, couples the object to one chosen invariant: representation changes propagate through types, equality transports appear, and the invalid or partially validated objects that exist in the real system must be represented outside the intrinsically valid fragment. This is why experienced users of dependent type theories do not put every invariant into a type — Lean developments routinely use ordinary datatypes with predicates and theorem hypotheses, and represent failure and partiality explicitly.<br>This suggests a useful engineering rule:<br>Put cheap, stable, compositional distinctions in types. Express contextual, evolving, and relational facts as propositions.

Dependent type theory lets a development move that boundary in either direction; HOL fixes it conservatively. The loss is that HOL cannot exploit dependency even where it would give an elegant local interface. The gain is that dependent...