"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.
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...
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.
> 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 ;)
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.
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.
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. :)
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.
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...
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.
I found the first version much more useful so I'm posting it here for others.