Comparing Coq (pCUIC) with HoTT and CubicalTT for common verification tasks

Using Coq
1

Homotopy type theory (HoTT) and Cubical type theory (CubicalTT) have been used to formalize foundations of mathematics, and have inspired extensions to Coq such as SProp.

However, demonstrated applications of HoTT and CubicalTT in regular verification tasks, such as for program verification, are to my knowledge few (e.g., SQL rewriting, patch theory, encoding pi-calculus, and probabilistic programming), and the general extent to which univalence increases the productivity of proof engineers is unknown.

Based on a discussion with @spitters on Coq’s Gitter, I would like to raise the issue of finding relevant benchmarks and case studies for comparing verification using vanilla Coq (pCUIC), HoTT for Coq, and Cubical Agda.

Interesting hard measures to compare include:

  • lines of spec code
  • lines of proof script code
  • effort to complete in person hours

Softer measures such as reusability, comprehensibility, extendability could also be considered.

Here are some candidates for benchmarks:

The comparison approach could be similar to a code golfing competition, i.e., the goal is to get definitions and proofs that are as elegant and short as possible.

The literature contains many comparisons of different systems for specific verification tasks that can provide inspiration, e.g., correctness of a graph algorithm by Tarjan in Coq, Why3, and Isabelle/HOL.

1 Like
2

One motivation in our guarded HoTT project and the related project by Møgelberg is to find a type theory that is more suitable for modelling projects like iris, but also coinduction. We are not there yet, but type theories such as guarded cubical type theory are conjectured to have good computational properties, as opposed to the (extensional) guarded dependent type theory which was used before.

I recently had two students implement Queues (as in Sec 5.2 of Okasaki) in cubical using HITs. This looks quite natural. I’ll see whether it can be made available.

1 Like
3

Queues

4

Nice @spitters, I may be out of my depth here, but would it be “fair” for comparison purposes (and at all possible) to capture the higher inductive type approach for the batched queue in vanilla Coq using private inductives? Or is an alternate vanilla Coq version using only “plain inductive types” the most reasonable?

5

Yes, I think a similar approach would work in Coq HoTT encoding HITs as private inductives.

1 Like