The Coq mailing list

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

Hi Jesper,

I will admit that my experience with those systems is limited, but 
nevertheless:
for the kind of proofs I am typically doing, the proof terms are *huge* and
mostly uninteresting.  Things like Iris <https://iris-project.org/> would, I
think, be entirely unfeasible in a system like Agda that makes you write proof
terms with your bare hands.
For such cases, you want a tactic language, and at that point you lose any
resemblance of uniformity. And in my experience, that applies to the majority 
of
things people do in Coq. (Also, the OP is using Coq, so it would be strange 
for
Jason to make an argument that doesn't actually apply to his work. ;)

Sure, there are things you can do to make writing proof terms less painful 
than
it is in Coq, but how far will that scale?

; Ralf

On 04.03.20 17:21, Jesper Cockx wrote:
> 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
> <mailto: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>
>     > 
> <mailto: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>
>     >     
> <mailto: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/
> 

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