In dependently-typed languages like Agda, it is possible to prove correctness of a function with respect to some propositional specification, represented as a type. One approach to program correctness adds the constraint that all specifications are of the form

f : a₁ → a₂ → ⋯ → aₙ → b
⟦_⟧ : b → z
⟦_⟧ᵢ : aᵢ → z
f' : z → z → ⋯ → z
⟦ f x₁ x₂ ⋯ xₙ ⟧ ≡ f' ⟦ x₁ ⟧₁ ⟦ x₂ ⟧₂ ⋯ ⟦ xₙ ⟧ₙ

where f is the n-ary function whose correctness we are checking, and ⟦_⟧ is the denotation. I first read of this approach in the work of Conal Elliott, who seems to have made fantastic progress in deriving “nice” implementations from such possibly noncomputable specifications. N.B.: I cannot be sure I have formulated the problem statement with appropriate generality.

As an example, again drawing from Elliott, we have the following specification for bitvector addition:

⊕-correctness : {m n : ℕ} → (xs : Vec Bool m) → (ys : Vec Bool n) → ⟦ xs ⊕ ys ⟧ ≡ ⟦ xs ⟧ + ⟦ ys ⟧

Given a function f, this approach reduces the problem of finding a specification to the problem of choosing the type b along with the data:

⟦_⟧ : b → z
⟦_⟧ᵢ : aᵢ → z
f' : z → z → ⋯ → z

This flavor of correct programming/formal verification can be done in an dependently-typed setting, but it leaves open the possibility of writing functions without proofs-of-correctness.

One might wonder if this is the best we can do.

My questions are: (1) is it possible to enforce at the level of the compiler the constraint that every function has a specification of the form (z, ⟦_⟧, {⟦_⟧ᵢ}ᵢ,f'), and (2) what constraints are necessary to avoid trivial or degenerate specifications?

To the second question, I have some partial answers based on intuition. We do not want z to be anything too small, so we might exclude the unit type. We also may not want z = b, which makes ⟦_⟧ = id. We also probably want f' to use all its arguments in most cases.

Possibly denotations are always unary, and I suppose there may be some measure of complexity of a type’s definition (perhaps recursively counting the number of constructors used to define it, or something like cyclomatic complexity?), and perhaps a denotation must always map into a type of lesser complexity.

Also, for “really fundamental” definitions, like + over the naturals, we may not be able to do this, and so we’d either need a principled way of distinguishing between foundational definitions and other things, or some kind of escape hatch.

The aim of such an implementation would be to produce a compiler which makes it very difficult to write incorrect programs. You’d be left with something like a “commutative programming language”, since every definition apart from those we mark as “axiomatic” must form a commutative diagram with the associated denotations for its type parameters.

Very happy to be pointed to prior work!