The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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/