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

**URL:** <https://discourse.rocq-prover.org/t/comparing-coq-pcuic-with-hott-and-cubicaltt-for-common-verification-tasks/598>\
**Category:** Using Rocq\
**Tags:** cic\
**Created:** [February 3, 2020, 4:41pm UTC](https://discourse.rocq-prover.org/t/comparing-coq-pcuic-with-hott-and-cubicaltt-for-common-verification-tasks/598 "2020-02-03T16:41:15Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [February 3, 2020, 4:41pm UTC](https://discourse.rocq-prover.org/t/comparing-coq-pcuic-with-hott-and-cubicaltt-for-common-verification-tasks/598/1 "2020-02-03T16:41:16Z")

</div>

[Homotopy type theory](https://homotopytypetheory.org) (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](https://homotopytypetheory.org/2016/09/26/hottsql-proving-query-rewrites-with-univalent-sql-semantics/), [patch theory](https://www.cs.cmu.edu/~cangiuli/papers/hpt-expanded.pdf), [encoding pi-calculus](https://niccoloveltri.github.io/cpp20.pdf), and [probabilistic programming](https://arxiv.org/abs/1912.07339)), 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](https://github.com/HoTT/HoTT), and [Cubical Agda](https://github.com/agda/cubical).

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:

- correctness of abstract data type implementations and algorithms from Okasaki’s book [Purely Functional Data Structures](https://www.cambridge.org/core/books/purely-functional-data-structures/0409255DA1B48FA731859AC72E34D494) (several of these have already been [done for HOL4](https://github.com/CakeML/cakeml/tree/master/translator/okasaki-examples) in CakeML)
- definitions and (category) theory from the book [Algebra of Programming](https://www.cs.ox.ac.uk/publications/publication2634-abstract.html) by Bird and de Moor (some of this has already been done in [plain Agda](https://github.com/scmu/aopa))
- metatheory and examples for some powerful modal logic, such as the [modal μ-calculus](https://en.wikipedia.org/wiki/Modal_%CE%BC-calculus), e.g., as presented by [Bradfield and Stirling](https://homepages.inf.ed.ac.uk/jcb/Research/MLH-bradstir.pdf)

The comparison approach could be similar to a [code golfing competition](https://meta.stackexchange.com/questions/20736/what-is-code-golf-on-stack-overflow), 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](https://arxiv.org/abs/1810.11979) in Coq, Why3, and Isabelle/HOL.

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [February 3, 2020, 5:15pm UTC](https://discourse.rocq-prover.org/t/comparing-coq-pcuic-with-hott-and-cubicaltt-for-common-verification-tasks/598/2 "2020-02-03T17:15:13Z")

</div>

One motivation in our [guarded HoTT](https://cs.au.dk/~birke/ghott/index.html) project and the related project by [Møgelberg](http://www.itu.dk/~mogel/) 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.

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [February 4, 2020, 9:36am UTC](https://discourse.rocq-prover.org/t/comparing-coq-pcuic-with-hott-and-cubicaltt-for-common-verification-tasks/598/3 "2020-02-04T09:36:03Z")

</div>

[Queues](https://github.com/limemloh/CubicalAgda-BatchedQueue)

---

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [February 4, 2020, 9:42am UTC](https://discourse.rocq-prover.org/t/comparing-coq-pcuic-with-hott-and-cubicaltt-for-common-verification-tasks/598/4 "2020-02-04T09:42:38Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![spitters](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/spitters/32/125_2.png) [@spitters](https://discourse.rocq-prover.org/u/spitters)\
**Post date:** [February 12, 2020, 3:37pm UTC](https://discourse.rocq-prover.org/t/comparing-coq-pcuic-with-hott-and-cubicaltt-for-common-verification-tasks/598/5 "2020-02-12T15:37:04Z")

</div>

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