Ebfer

Version 0.1 | See also: Lome ∘ Eqthy

Work in progress

Ebfer is a simple, dynamically typed, pure functional programming language. Embedded within Ebfer is an extremely simple proof language Footnote 1. Although this proof language may be used on its own, it is intended to be used to write embedded proofs of properties of the functions of the Ebfer program, in a manner similar to unit tests or QuickCheck tests. However, these aren't just tests; they are proofs. And their existence isn't due to the Curry-Howard correspondence in a dependently typed setting; the language is dynamically typed.

Ebfer's embedded proof language is currently a tiny, explicit proof language called Lome, which is defined separately, in its own repository.

Here is a example Ebfer program where we define a perimeter function, then give a proof showing that this function commutes:

fun perim(W, L) => add(mul(W, 2), mul(L, 2))
fun main() => perim(50, 33)

rule mul_comm(mul(A, B)) => mul(B, A)
rule add_comm(add(A, B)) => add(B, A)

theorem
    perim_comm(perim(W, L)) => perim(L, W)
proof
    *perim_expand(perim(W, L))
    add(mul(W, 2), mul(L, 2))
    *add_comm(add(mul(W, 2), mul(L, 2)))
    add(mul(L, 2), mul(W, 2))
    *perim_contract(add(mul(L, 2), mul(W, 2)))
    perim(L, W)
qed

For the full definition of the Ebfer language, see doc/Ebfer.md.

Future Work

Lome can handle simple equational reasoning, and the above example show how it plays out inside Ebfer. But to tackle really interesting properties of functions, the proof system would need to handle recursive functions, and this would necessitate:

• Proof under an assumption, including discharging the assumption (a la natural deduction).
• Proof by cases.
• Proof by structural induction (a combination of the previous two.)

Some — maybe even most — of this can be done with Lome (see the notes in eg/assume-discharge.ebfer for some work in this area), but a certain amount of "substructual futzing" is involved, and that "certain amount" is probably excessive for practical work. No one wants to spend half their proof just shuttling terms around.

But this directly contradicts Lome's goals of being radically simple and explicit. Footnote 2.

So it feels like there are two paths, and it's not yet clear which one Ebfer will take:

• Ebfer could adopt a richer, less low-level proof language as its embedded proof language. This could depart as far as we like from Lome, adding support for whatever proof methods we like, at the cost of more complexity in the codebase.
• We could discover some clever ways to get around, or at least mitigate, Lome's limitations, possibly in an intermediate layer between Ebfer and Lome. Lome's explicit nature does closely align with functional programming and it seems possible there is some way to write "tactics" in the functional language and "wedge" them in during the proof process, although it's not yet clear what that would look like.

The latter is more interesting as a research pathway, but also far more challenging (and this is probably not a coincidence).

Footnotes

Footnote 1

A "proof language" in this sense is a computer language in which theorems can be stated and mechanically checked by a computer. And a "computer language" in this sense is a rigorously-defined, machine-processable data format which can be read and written by humans using common text editing software.

Footnote 2

It also highlights one difference between tests and proofs: it's much easier to write a black-box test than a black-box proof, because proofs have to ultimately thread through the definitions, and those definitions will be concrete, unless you've put in the work to build a layer of abstract definitions on top of them — and even then, that only reduces the "contact area", it doesn't eliminate it. Any change to the implementation will necessitate updating the proof. (You can really see why people like to focus on proof automation.) In order to not become burdensome to development, sets of "unit proofs" would need to be designed to minimize those needed changes — although I suspect the result design would also be generally preferable for ergonomic reasons.