Coq: Certified Programming with Dependent Types | Hacker News Reader

Coq: Certified Programming with Dependent Types

adam.chlipala.net

107 pointslobo_tuerto33 comments

I found 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

I found the first version much more useful so I'm posting it here for others.

Worth noting, lest the name scare you away from a great computer science achievement:

https://coq.inria.fr/news/114.html

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.

FTR, I've learned Coq before Haskell

I learned ML -> Coq -> Haskell. Still working on getting really good at Haskell.

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...

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

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.

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.

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.

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.

> 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

It depends how complex the algorithms are. You would need to write a specification* and an implementation; there's not much point unless the specification is much simpler than the implementation. For example, if the specification of the tax software says things like:

    If the FOO is less than 1000, then BAR is 12. If FOO is greater than or equal to 1000 then BAR is 20.

Then there's not much point using Coq: the specification is basically a step-by-step description of what to execute. All you need to do is rewrite it in a machine-readable form. You're just as likely to make mistakes translating it to Coq's specification (type) language as you are translating it straight to, eg., Haskell.

If the specification less algorithmic, then it might be useful. For example, if it dictates things like:

    The sum of FOO and BAR should never exceed BAZ.
    QUUX can increase or decrease by 10% each year, providing that the difference between year N and year N+5 is less than 5%, and that there are no consecutive increases of length 3 or more.

Then you might consider implementing the core calculations in a language like Coq. Once you've proven your algorithms correct, you can "extract" them into some other language, eg. in Haskell, and call out to that from your regular code.

> or do you somehow use Coq to prove that your eg. C++ code is correct?

That's far too difficult at the moment. You could use Coq to prove the correctness of some algorithm or protocol or whatever, in an abstract form, then go off and implement that algorithm in C++. You would have no guarantees that the C++ is correct (ie. whether it implements the algorithm/protocol faithfully); all you would know is that you're not wasting time trying to implement a flawed algorithm :)

* Well, you don't need to write a specification, but there's no point using Coq otherwise ;)

Great explanation. Many thanks.

You might gain a lot... just not much that is practical to web development. However great ideas are not born in a vacuum and generating new ones often come from being exposed to others. It couldn't hurt if you have the time and interest.

I know I replied in another thread but Ur/Web uses a rich type system to make reliable web applications. Just popped into my head. Opa language does too. Check them out.

http://plv.csail.mit.edu/ur/

http://opalang.org/

Addendum: the author of Ur/Web is the same person as the author of the linked book.

Good catch! Forgot to mention it. Yeah, Chlipala certainly practices what he preaches by building lots of useful tools for the rest of us using the very methods he writes about. Moreover, tools that catch or prevent lots of problems in other useful apps or tools. The kind of researcher and research we can always use more of. :)

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

Does Software Foundations assume a less or more advanced background from its readers?

Far less, IMO.

Software foundations is very introductory level text on Coq which is very accessible for people without formal proof experience.

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

It originated in France (see 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...

The language and ideas behind it seems pretty serious. But they might consider pissing off particularly prudish Americans to be a bonus.

A few timid speakers will mispronounce it like "coke", but everyone knows they're saying it wrong.

It's pronounced identically to "caulk", though, not "cock".

More like somewhere in between, really.

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".

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

this link seems to agree, with the word represented in IPA as [kɔːk]

More information about who in the US has and hasn't merged those two sounds: https://en.wikipedia.org/wiki/Phonological_history_of_Englis...

It's the cot-caught merger.

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

> 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.

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 ;)

Reply on news.ycombinator.com