Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A short introduction to Coq

coq.inria.fr

Post reply on HN
Print view View original

1–10 of 13 posts

Re: A short introduction to Coq

#6

Post by pascal_cuoq »

Every time someone points out this tutorial and I see again the even_0 and even_S constructors of the even predicate, I am reminded of the quote where FORTRAN is called a high-level language because, unlike assembly, it doesn't force the programmer to make up names for intermediate expressions.

There are good reasons why even_0 and even_S need to have names, but I sure hope that we will one day look back on Coq as the assembly of computer-assisted proofs.

Re: A short introduction to Coq

#7

Post by scscsc »

pascal_cuoq wrote: post #6

Every time someone points out this tutorial and I see again the even_0 and even_S constructors of the even predicate, I am reminded of the quote where FORTRAN is called a high-level language because, unlike assembly, it doesn't force the programmer to make up names for intermediate expressions. There are good reasons why even_0 and even_S need to have names, but I sure hope that we will one day look back on Coq as th…

I somewhat agree. I have a stronger postulate: current proof assistants are worse for writing proofs than machine language.

There is a reason not to panic: it can only get better, not worse...

Re: A short introduction to Coq

#8

Post by jbapple »

pascal_cuoq wrote: post #6

Every time someone points out this tutorial and I see again the even_0 and even_S constructors of the even predicate, I am reminded of the quote where FORTRAN is called a high-level language because, unlike assembly, it doesn't force the programmer to make up names for intermediate expressions. There are good reasons why even_0 and even_S need to have names, but I sure hope that we will one day look back on Coq as th…

pascal_cuoq said: "There are good reasons why even_0 and even_S need to have names, but I sure hope that we will one day look back on Coq as the assembly of computer-assisted proofs."

For predicates that can be computed in coq, we can do away with the names:

  Fixpoint even n :=
    match n with
      | 0 => True
      | 1 => False
      | S (S m) => even m
    end.
Note that "True" and "False" are propositions (have sort "Prop") with trivial and no proofs, respectively, and are not "true" and "false", which are the constructors of the inductive type "bool". If the return type were changed to bool, "even n = true" (rather than just "even n") would be a predicate meaning "n is an even natural number".

Additionally, your wish is already coming true! For certain types of problems, coq can be hooked up to external solvers (for SAT, for instance) which generate proof terms that are then checked by coq. See http://www.lri.fr/~melquion/doc/09-calculemus-article.pdf for an example.

Re: A short introduction to Coq

#9

Post by maxklein »

lallysingh wrote: post #2

Sorry, I have to ask -- it's the reddit/adolescent in me. What's the proper way to pronounce the name?

I mean, seriously, I'd never specialise in this language because everyone will turn to a teenager when you are listing your skills.

You are really good at coq? So, what's your favorite thing about coq? Do you guys ever have coq meetups?

Naming is important.

Re: A short introduction to Coq

#10

Post by jbapple »

maxklein wrote: post #9
lallysingh wrote: post #2

Sorry, I have to ask -- it's the reddit/adolescent in me. What's the proper way to pronounce the name?

I mean, seriously, I'd never specialise in this language because everyone will turn to a teenager when you are listing your skills. You are really good at coq ? So, what's your favorite thing about coq ? Do you guys ever have coq meetups? Naming is important.

maxklein said: "I'd never specialise in this language because everyone will turn to a teenager when you are listing your skills."

Coq is not a general-purpose programming language. People who "specialize in this language" generally work in a field where everyone is familiar with the name "coq" and nobody bats an eye.

Post reply on HN