The Coq mailing list

[Jesper Cockx <Jesper AT sikanda.be>]

Hi Ralf,

There are other dependently typed languages besides Coq that do provide a unified language for programs and proofs ;)

-- Jesper

On Wed, Mar 4, 2020 at 5:10 PM Ralf Jung <jung AT mpi-sws.org> wrote:

Hi Jesper,

I agree with most of your points, but...

> - From a practical point of view, in a dependently typed language I don't have to learn and use separate languages for writing programs and for writing proofs about them. In fact, by giving the write types to my programs I often do not need to give any proofs at all (i.e. correct-by-construction programming).

Practically speaking, in Coq, programs are written in Gallina and proofs are
written in Ltac.  These two languages could hardly be more different.

; Ralf

On 03.03.20 22:37, Jesper Cockx wrote:
> Hi Jason,
>
> There's many reasons for me to choose a dependently typed language:
>
> - From a philosophical point of view, dependently typed languages are the only
> kind of language that have been given a meaning explanation (in the sense of
> Martin-Löf). This is important because it means I can grasp the meaning of each
> rule/axiom on a fundamental level, something that I never managed for set theory.
> - From a practical point of view, in a dependently typed language I don't have
> to learn and use separate languages for writing programs and for writing proofs
> about them. In fact, by giving the write types to my programs I often do not
> need to give any proofs at all (i.e. correct-by-construction programming).
> - Dependent type theory is constructive so I do not have to assume classical
> principles when I do not need them.
> - Since expressions at the type level can compute in dependent type theory,
> there are many equalities that I do not need to reason about explicitly but just
> hold by definition/computation (although not as many as I would want).
>
> As for other interactive theorem provers not based on dependent type theory,
> such as Isabelle or HOL4, I am mainly jealous of their excellent integration
> with automated theorem proving tools (e.g. sledgehammer) and their huge
> mathematical libraries. In a dependently typed languages, it is much harder to
> get everyone to agree on a definition because there are so many different ways
> to encode a concept. This has the effect that libraries are a lot more
> fragmented and everything is done in a more ad-hoc manner.
>
> Another weak point of current implementations of dependent type theory is
> abstraction: you /can/ make a definition abstract but that means it becomes an
> inert lump that stubbornly refuses to compute, so you lose most of the benefits
> of working with a dependently typed language. But I see these as reasons to
> continue to improve dependently typed languages rather than to abandon them.
>
> -- Jesper
>
> On Tue, Mar 3, 2020 at 10:00 PM Viktor Kunčak <vkuncak AT gmail.com
> <mailto:vkuncak AT gmail.com>> wrote:
>
>     I would be also curious to hear answers to this questions!
>     ("Lots of people do it" seems like a very compelling answer.)
>
>     Which bottlenecks are you referring to? Are they intrinsically tied to
>     dependent types, or they are related to the treatment of propositions and
>     equality in systems such as Coq?
>
>     There are type systems overlayed on top of initially untyped languages (e.g.
>     the language of Alloy Analyzer) and there are gradual types and designs like
>     TypeScript for to initially untyped programming languages. ACL2 theorem
>     prover for pure LISP, SPASS theorem prover for first-order logic, and "TLA+
>     model checking made symbolic" model checker for TLA+ all include techniques
>     to recover types from an initially untyped language.
>
>     Best regards,
>
>       Viktor
>
>     On Tue, Mar 3, 2020 at 8:44 PM Jason Gross <jasongross9 AT gmail.com
>     <mailto:jasongross9 AT gmail.com>> wrote:
>
>         I'm in the process of writing my thesis on proof assistant performance
>         bottlenecks (with a focus on Coq), and there's a large class of
>         performance bottlenecks that come from (mis)using the power of dependent
>         types.  So in writing the introduction, I want to provide some
>         justification for the design decision of using dependent types, rather
>         than, say, set theory or classical logic (as in, e.g., Isabelle/HOL). 
>         And the only reasons I can come up with are "it's fun" and "lots of
>         people do it"
>
>         So I'm asking these mailing lists: why do we base proof assistants on
>         dependent type theory?  What are the trade-offs involved?
>         I'm interested both in explanations and arguments given on list, as well
>         as in references to papers that discuss these sorts of choices.
>
>         Thanks,
>         Jason
>

--
Website: https://people.mpi-sws.org/~jung/