6 ms·

Coq: Certified Programming with Dependent Types

107 points by lobo_tuerto 11y ago

bencollier49 11y ago
I assume that this wasn't originally created by an English-speaking dev team? Or at least a very serious and formal one?
- liotier 11y ago
  It originated in France (see https://coq.inria.fr/about-coq https://coq.inria.fr/about-coq). In French, 'coq' means 'rooster' - the language that implements Coq is named Gallina and the logo is indeed a rooster. Well, no worse an homophone than 'bit' to French speakers...
- throwaway999666 11y ago
  The language and ideas behind it seems pretty serious. But they might consider pissing off particularly prudish Americans to be a bonus.
  - justinpombrio 11y ago
    A few timid speakers will mispronounce it like "coke", but everyone knows they're saying it wrong.
    - eli_gottlieb 11y ago
      It's pronounced identically to "caulk", though, not "cock".
      - davidgay 11y ago
        More like somewhere in between, really.
      - davidgrenier 11y ago
        Not 100% confident on how people pronounce "cock" but it's definitely not close to "caulk". Being a french speaker, I would say pronunciation is closer to "puck" with a k, so go with "Kuck".
      - Afton 11y ago
        In my idiolect, those two words are homonyms. When I worked construction, you couldn't ask someone for caulk without raucous laughter. http://dictionary.reference.com/browse/caulk http://dictionary.reference.com/browse/caulk this link seems to agree, with the word represented in IPA as [kɔːk]
      - innguest 11y ago
        More information about who in the US has and hasn't merged those two sounds: https://en.wikipedia.org/wiki/Phonological_history_of_English_low_back_vowels#Cot.E2.80.93caught_merger https://en.wikipedia.org/wiki/Phonological_history_of_Englis... It's the cot-caught merger.
  - cjensen 11y ago
    Intentionally pissing off people is childish. Using the name of this language in a workplace creates a hostile working environment[1]. That guarantees that no sensible person in the English speaking world will ever use the language at work. [1] https://en.wikipedia.org/wiki/Hostile_work_environment https://en.wikipedia.org/wiki/Hostile_work_environment
    - throwaway999666 11y ago
      > Using the name of this language in a workplace creates a hostile working environment[1]. Oh my, thanks for the laugh. I half imagined a Dilbert scenario when reading that. It's weird to think of the simultaneous uptightness and childishness which would make it impossible to use this homonym in the proper context.
- groar 11y ago
  There are many reasons for the name: apart from being one of France's emblems, one of the people who initiated the project is Thierry Coquand and the original type system underlying it is called Calculus Of Construction (CoC). But I know for a fact that they thought it would be good joke as well. Or at least a very [...] formal one That's a good one ;)
reirob 11y ago
From the Intro, the prerequisites: "I try to keep the required background knowledge to a minimum in this book. I will assume familiarity with the material from usual discrete math and logic courses taken by undergraduate computer science majors, and I will assume that readers have significant experience programming in one of the ML dialects, in Haskell, or in some other, closely related language. Experience with only dynamically typed functional languages might lead to befuddlement in some places, but a reader who has come to understand Scheme deeply will probably be fine." Then it is not for me, I am still struggling with Haskell.
- gclaramunt 11y ago
  FTR, I've learned Coq before Haskell
- eli_gottlieb 11y ago
  I learned ML -> Coq -> Haskell. Still working on getting really good at Haskell.
userbinator 11y ago
The code appears to be presented in a mix of fixed-width, proportional, italic, bold, and sans-serif fonts, with a bit of colour thrown in. I don't think that's particularly readable...
solomatov 11y ago
It's the best (and only) intermediate level Coq book around.
- throwaway999666 11y ago
  Does Software Foundations assume a less or more advanced background from its readers?
  - curryhoward 11y ago
    Far less, IMO.
  - solomatov 11y ago
    Software foundations is very introductory level text on Coq which is very accessible for people without formal proof experience.
weavie 11y ago
So would a bog standard web developer gain anything by learning Coq? Or is it something just for academics?
- chriswarbo 11y ago
  If you're just plugging together library components to produce regular CRUD sites, then it won't have any direct relevance. Hopefully those components will have strong types to make sure they're being used in valid ways, but that's about as far as it's worth going. If you're building those libraries, then you might want to use some clever type system tricks to bridge the gap between a friendly external API and an internal representation with strong guarantees. Some of those clever tricks might be done with dependent types, and you might use Coq to do them. If you're building core infrastructure stuff, like crypto libraries, communication protocols, data storage/retrieval, language interpreters, etc. where something as trivial as an off-by-one error might cause large problems, then you might benefit from using Coq to formally prove that your implementations satisfy their specification.
  - weavie 11y ago
    I see. Quite often regular CRUD sites have business logic in them. Stuff such as Tax software has very rigid logic - the stronger guarantees you can make as to their correctness the better. So would you actually write the library in Coq - or do you somehow use Coq to prove that your eg. C++ code is correct? I've not come across any libraries written in Coq yet.
    - wk_end 11y ago
      Coq doesn't really provide a suitable environment for executing real software AFAIK; it's designed so that, once you've proven your code correct, it can extract a Haskell or Ocaml program out of it.
    - nickpsecurity 11y ago
      The best language for that is Ada 2012 which now has Design by Contract. There's tools, such as SPARK, to throughly prove or test it free of many problems. Eiffel has had Design-by-Contract for a while, but I'm not familiar with its tools. There's tools for similarly interface and implementation checking C, C#, and Java programs. So, best route is one of these languages with the tools, good coding guidelines, and formal inspections of design/code/docs for common issues.
infruset 11y ago
Worth noting, lest the name scare you away from a great computer science achievement: https://coq.inria.fr/news/114.html https://coq.inria.fr/news/114.html
- deleted 11y ago
  [deleted]
kestert 11y ago
I found http://adam.chlipala.net/cpdt/html/Hoas.html http://adam.chlipala.net/cpdt/html/Hoas.html to be very useful. It looks like it was once a chapter of the book, but was replaced by the final chapter http://adam.chlipala.net/cpdt/html/ProgLang.html http://adam.chlipala.net/cpdt/html/ProgLang.html I found the first version much more useful so I'm posting it here for others.

107 points by lobo_tuerto 11y ago

I assume that this wasn't originally created by an English-speaking dev team? Or at least a very serious and formal one?

liotier 11y ago
It originated in France (see https://coq.inria.fr/about-coq https://coq.inria.fr/about-coq). In French, 'coq' means 'rooster' - the language that implements Coq is named Gallina and the logo is indeed a rooster. Well, no worse an homophone than 'bit' to French speakers...
throwaway999666 11y ago
The language and ideas behind it seems pretty serious. But they might consider pissing off particularly prudish Americans to be a bonus.
- justinpombrio 11y ago
  A few timid speakers will mispronounce it like "coke", but everyone knows they're saying it wrong.
  - eli_gottlieb 11y ago
    It's pronounced identically to "caulk", though, not "cock".
    - davidgay 11y ago
      More like somewhere in between, really.
    - davidgrenier 11y ago
      Not 100% confident on how people pronounce "cock" but it's definitely not close to "caulk". Being a french speaker, I would say pronunciation is closer to "puck" with a k, so go with "Kuck".
    - Afton 11y ago
      In my idiolect, those two words are homonyms. When I worked construction, you couldn't ask someone for caulk without raucous laughter. http://dictionary.reference.com/browse/caulk http://dictionary.reference.com/browse/caulk this link seems to agree, with the word represented in IPA as [kɔːk]
    - innguest 11y ago
      More information about who in the US has and hasn't merged those two sounds: https://en.wikipedia.org/wiki/Phonological_history_of_English_low_back_vowels#Cot.E2.80.93caught_merger https://en.wikipedia.org/wiki/Phonological_history_of_Englis... It's the cot-caught merger.
- cjensen 11y ago
  Intentionally pissing off people is childish. Using the name of this language in a workplace creates a hostile working environment[1]. That guarantees that no sensible person in the English speaking world will ever use the language at work. [1] https://en.wikipedia.org/wiki/Hostile_work_environment https://en.wikipedia.org/wiki/Hostile_work_environment
  - throwaway999666 11y ago
    > Using the name of this language in a workplace creates a hostile working environment[1]. Oh my, thanks for the laugh. I half imagined a Dilbert scenario when reading that. It's weird to think of the simultaneous uptightness and childishness which would make it impossible to use this homonym in the proper context.
groar 11y ago
There are many reasons for the name: apart from being one of France's emblems, one of the people who initiated the project is Thierry Coquand and the original type system underlying it is called Calculus Of Construction (CoC). But I know for a fact that they thought it would be good joke as well. Or at least a very [...] formal one That's a good one ;)

reirob 11y ago

From the Intro, the prerequisites: "I try to keep the required background knowledge to a minimum in this book. I will assume familiarity with the material from usual discrete math and logic courses taken by undergraduate computer science majors, and I will assume that readers have significant experience programming in one of the ML dialects, in Haskell, or in some other, closely related language. Experience with only dynamically typed functional languages might lead to befuddlement in some places, but a reader who has come to understand Scheme deeply will probably be fine." Then it is not for me, I am still struggling with Haskell.

gclaramunt 11y ago
FTR, I've learned Coq before Haskell
eli_gottlieb 11y ago
I learned ML -> Coq -> Haskell. Still working on getting really good at Haskell.

userbinator 11y ago

The code appears to be presented in a mix of fixed-width, proportional, italic, bold, and sans-serif fonts, with a bit of colour thrown in. I don't think that's particularly readable...

solomatov 11y ago

It's the best (and only) intermediate level Coq book around.

throwaway999666 11y ago
Does Software Foundations assume a less or more advanced background from its readers?
- curryhoward 11y ago
  Far less, IMO.
- solomatov 11y ago
  Software foundations is very introductory level text on Coq which is very accessible for people without formal proof experience.

weavie 11y ago

So would a bog standard web developer gain anything by learning Coq? Or is it something just for academics?

chriswarbo 11y ago
If you're just plugging together library components to produce regular CRUD sites, then it won't have any direct relevance. Hopefully those components will have strong types to make sure they're being used in valid ways, but that's about as far as it's worth going. If you're building those libraries, then you might want to use some clever type system tricks to bridge the gap between a friendly external API and an internal representation with strong guarantees. Some of those clever tricks might be done with dependent types, and you might use Coq to do them. If you're building core infrastructure stuff, like crypto libraries, communication protocols, data storage/retrieval, language interpreters, etc. where something as trivial as an off-by-one error might cause large problems, then you might benefit from using Coq to formally prove that your implementations satisfy their specification.
- weavie 11y ago
  I see. Quite often regular CRUD sites have business logic in them. Stuff such as Tax software has very rigid logic - the stronger guarantees you can make as to their correctness the better. So would you actually write the library in Coq - or do you somehow use Coq to prove that your eg. C++ code is correct? I've not come across any libraries written in Coq yet.
  - wk_end 11y ago
    Coq doesn't really provide a suitable environment for executing real software AFAIK; it's designed so that, once you've proven your code correct, it can extract a Haskell or Ocaml program out of it.
  - nickpsecurity 11y ago
    The best language for that is Ada 2012 which now has Design by Contract. There's tools, such as SPARK, to throughly prove or test it free of many problems. Eiffel has had Design-by-Contract for a while, but I'm not familiar with its tools. There's tools for similarly interface and implementation checking C, C#, and Java programs. So, best route is one of these languages with the tools, good coding guidelines, and formal inspections of design/code/docs for common issues.

infruset 11y ago

Worth noting, lest the name scare you away from a great computer science achievement: https://coq.inria.fr/news/114.html https://coq.inria.fr/news/114.html

deleted 11y ago
[deleted]

kestert 11y ago

I found http://adam.chlipala.net/cpdt/html/Hoas.html http://adam.chlipala.net/cpdt/html/Hoas.html to be very useful. It looks like it was once a chapter of the book, but was replaced by the final chapter http://adam.chlipala.net/cpdt/html/ProgLang.html http://adam.chlipala.net/cpdt/html/ProgLang.html I found the first version much more useful so I'm posting it here for others.