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