> The purity of Coq ensures that each request is answered exactly once in finite time.<p>How does Coq ensure that the request completes in finite time?
Not to diminish the accomplishment, I think it is really cool, but I won't say "I'd buy that for a dollar." A blog engine with provably correct posts and comments though? That's a real kickstarter. Although the use case might not be the internet as we know it.<p>But require the comments to be provably correct and assume the post as premise and I think we're onto a winner.
The last line threw me off:<p>> an unauthenticated user cannot access private pages (like edit) or modify the file system with system calls.<p>System calls? How do they come into the picture? And wouldn't reasoning about system calls require proofs about the kernel itself?
Is there a good practical resource for learning about applying formal proof systems like Coq or Spin, but for those without a CS background? I'm interested in provably correct systems, but a lot of the material seems to be heavy on the theoretical side. I guess you could say I'm searching for the <i>Art of Electronics</i>, but for formal proofs.
disclaimer: outside of a quick understanding of what "formal proof system" is, I have no deep understanding of how it works.<p>It is written there's a Coq->OCaml compilation step. Would it be easily possible to have any Coq->other language (I'm mostly thinking about Rust) compiler ? Or do some properties of OCaml make it much easier (I mean "several order of magnitude") to implement than more 'common' dynamic languages like Php/Python/ruby ?
This quite cool but for an HTTP server, most requests should complete within a few seconds and the average should be in milliseconds. Proving that requests are handled in finite time is useful (some kinds of bugs are eliminated) but it's not really the performance guarantee that's needed in this domain. We will probably be using performance testing rather than proofs for a long time.