A blog engine written and proven in Coq(coq-blog.clarus.me)
coq-blog.clarus.me
A blog engine written and proven in Coq
http://coq-blog.clarus.me/a-blog-engine-written-and-proven-in-coq.html
9 comments
I haven't looked at the code but you can prove many functions in Coq terminate by showing they are structurally recursive. Concisely, you show a function only calls itself on smaller versions of the originally parameters so there must be a limit to how many recursive calls you can make.
For example, a function F to find the item X in the the list L might look like this:
1. If L is empty, return false.
2. If the front of L is X, return true.
3. Otherwise return the result of calling F on L with its front item removed.
The list must get smaller every recursive call so there's a limit to the recursion. Lots of functions recurse in this way (e.g. map, filter, reduce, max) and Coq can detect these automatically usually.
For more complicated cases, you can provide some numeric metric to Coq and write a proof that this metric must eventually reach some limit. For example, to prove quicksort terminates, you usually show the length of the lists called in the recursive calls are smaller each time.
So, in general, there's no procedure to show an arbitrary function terminates, but for the kind of functions people usually write, there are practical ways to prove termination.
For example, a function F to find the item X in the the list L might look like this:
1. If L is empty, return false.
2. If the front of L is X, return true.
3. Otherwise return the result of calling F on L with its front item removed.
The list must get smaller every recursive call so there's a limit to the recursion. Lots of functions recurse in this way (e.g. map, filter, reduce, max) and Coq can detect these automatically usually.
For more complicated cases, you can provide some numeric metric to Coq and write a proof that this metric must eventually reach some limit. For example, to prove quicksort terminates, you usually show the length of the lists called in the recursive calls are smaller each time.
So, in general, there's no procedure to show an arbitrary function terminates, but for the kind of functions people usually write, there are practical ways to prove termination.
In Coq all functions terminate.
Coq's correctness depends on termination. In Coq the propositions are types. To prove a proposition is to construct a program of this type. If one allowed non-termination, then it would be easy to construct a program of any type (like in OCaml let rec f() = f() has type () -> 'a), so you could prove anything.
Coq's correctness depends on termination. In Coq the propositions are types. To prove a proposition is to construct a program of this type. If one allowed non-termination, then it would be easy to construct a program of any type (like in OCaml let rec f() = f() has type () -> 'a), so you could prove anything.
I didn't say anything that disagrees with that...I was simply trying to give an easy to understand example for how you justify to a computer that a function will always terminate from the perspective of someone who has never used Coq or another theorem prover.
In this context, it's isn't very illuminating to tell a non-Coq user that all Coq functions terminate; formulating your function definition into something that Coq will accept is the difficult part.
In this context, it's isn't very illuminating to tell a non-Coq user that all Coq functions terminate; formulating your function definition into something that Coq will accept is the difficult part.
I see. You said "you can prove many functions in Coq terminate", so it seemed you were talking about functions written in Coq.
Ah, I meant that in the sense of, think of an algorithm you want to write, many of them are structurally recursive and they're straightforward to implement in Coq.
[deleted]
Coq isn't Turing complete - it has a termination checker that needs to be able to determine that your functions terminate.
Technically speaking, corecursion allows for writing Turing-complete programs, including nonterminating programs. It just requires that you explicitly specify where you use nontermination and prove that each iteration yields a well-typed result.
Yes, one can represent non-terminating programs. One can represent Turing machines as data, after all. But one cannot write a Coq function that will fully execute such programs. Each well-typed Coq function, when applied to concrete arguments, will terminate in a finite number of steps. One can implement the step function of a Turing Machine in Coq and one can write a function that runs a Turing Machine for k steps, but one cannot execute a Turing Machine for an unbounded number of steps.
[I guess that's what you're saying, but there seems to be some confusion here, so it's perhaps best to try to be explicit.]
[I guess that's what you're saying, but there seems to be some confusion here, so it's perhaps best to try to be explicit.]
> One can implement the step function of a Turing Machine in Coq and one can write a function that runs a Turing Machine for k steps, but one cannot execute a Turing Machine for an unbounded number of steps.
I know we can't execute an unbounded number of steps during compilation, but how does this work with program extraction? Can we extract a Haskell/Scheme/etc. program which implements our unbounded, corecursive step function?
I know we can't execute an unbounded number of steps during compilation, but how does this work with program extraction? Can we extract a Haskell/Scheme/etc. program which implements our unbounded, corecursive step function?
You can extract lazy values that represent infinite data. For example, you can define the stream of the factorial numbers as follows.
Even without corecursive data, you can define a function that for a given TM returns a function of type nat->state, which computes the state of the TM after k steps. In a way this value also represents the whole, possibly infinite, computation of the machine.
CoInductive Stream (T: Type): Type :=
Cons: T -> Stream T -> Stream T.
Fixpoint fac(n : nat): nat :=
match n with
| 0 => 1
| S n => n * (fac n)
end.
CoFixpoint facs : nat -> Stream nat :=
fun n =>
Cons (fac n) (facs (n+1)).
Definition fs := facs 0.
data Stream t =
Cons t (Stream t)
fac :: Nat -> Nat
fac n =
case n of {
O -> S O;
S n0 -> mul n0 (fac n0)}
facs :: Nat -> Stream Nat
facs n =
Cons (fac n) (facs (add n (S O)))
fs :: Stream Nat
fs = facs O
Even without corecursive data, you can define a function that for a given TM returns a function of type nat->state, which computes the state of the TM after k steps. In a way this value also represents the whole, possibly infinite, computation of the machine.
Not quite. IIRC, corecursive programs (and the coinductive data-types they return) are straightforwardly nonterminating: they can loop infinitely. The difference is that each iteration is proven to terminate and to yield a well-specified result, and arbitrary theorems can be proven about the generator function yielding each iteration's result.
http://www.cse.chalmers.se/research/group/logic/TypesSS05/Ex...
http://www.cse.chalmers.se/research/group/logic/TypesSS05/Ex...
At a guess it demonstrates that there's no possibility for infinite loops or recursion. It's going to rely on a model of the storage mechanism (memory, disk, whatever) that will respond to requests for data in finite time, but that doesn't seem an unreasonable assumption to make in this case. You have to draw the lines around your proof system somewhere or else you're going to end up having to model the entire world.
> that doesn't seem an unreasonable assumption to make in this case
Not that I don't agree with you but I find it a common failure mode of HDs to just never reply to things. I guess it's also a common failure mode of network systems too.
Can Coq detect that you are enforcing I/O timeouts in a way that guarantees finite time?
Not that I don't agree with you but I find it a common failure mode of HDs to just never reply to things. I guess it's also a common failure mode of network systems too.
Can Coq detect that you are enforcing I/O timeouts in a way that guarantees finite time?
I don't know whether this particular proof models IO timeouts - might have a poke at it and see what it's doing if I have time later.
More generally, Coq is "just" a well integrated proof tool & I can't see any reason why you couldn't include such features but at some point you have to draw the line and be explicit about what it is that you're actually proving: if your proof assumes data store responsiveness then it's OK for it to do that so long as you're explicit about the resulting limitations IMO. The goal of ever increasing model fidelity is a rabbit hole from which the programmer/prover might never return otherwise :)
More generally, Coq is "just" a well integrated proof tool & I can't see any reason why you couldn't include such features but at some point you have to draw the line and be explicit about what it is that you're actually proving: if your proof assumes data store responsiveness then it's OK for it to do that so long as you're explicit about the resulting limitations IMO. The goal of ever increasing model fidelity is a rabbit hole from which the programmer/prover might never return otherwise :)
Yes, for now we assume that there is exactly one answer for each external call to the system: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...
In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.
In practice, we should use a timeout in the implementation of all the external calls, but we did not and our model to not enforce it.
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.
But require the comments to be provably correct and assume the post as premise and I think we're onto a winner.
But require the comments to be provably correct and assume the post as premise and I think we're onto a winner.
> require the comments to be provably correct and assume the post as premise and I think we're onto a winner
It's trivial: proof is by EFQ. ;)
It's trivial: proof is by EFQ. ;)
An interesting idea. I've written an "active code" system for my blog, based on the excellent Pandoc ( http://chriswarbo.net/essays/activecode/index.html ) so I can write code inside my posts and have it executed during rendering.
There's no requirement to do things that way, but it's certainly possible to write posts containing blocks of Coq code and blocks of shell code for compiling them, such that a failed compilation will abort the rendering. In fact, I'm doing that very thing right now! Although I'm rendering a PDF paper rather than a HTML blog post ;)
There's no requirement to do things that way, but it's certainly possible to write posts containing blocks of Coq code and blocks of shell code for compiling them, such that a failed compilation will abort the rendering. In fact, I'm doing that very thing right now! Although I'm rendering a PDF paper rather than a HTML blog post ;)
The last line threw me off:
> an unauthenticated user cannot access private pages (like edit) or modify the file system with system calls.
System calls? How do they come into the picture? And wouldn't reasoning about system calls require proofs about the kernel itself?
> an unauthenticated user cannot access private pages (like edit) or modify the file system with system calls.
System calls? How do they come into the picture? And wouldn't reasoning about system calls require proofs about the kernel itself?
I guess this merely means that it is proven that no such system calls are executed directly.
Of course, in theory there might be some kernel bug such that e.g. a read() sometimes changes files on disk, but I guess this is outside the scope of that proof system. Only the blog program itself was proven, assuming that the remaining system software as well as hardware are working in a sane way.
If you want your proofs to include the whole operating system, you'd first have to reduce the kernel to a minimal operating system (e.g. MirageOS). If have lots of time, money and motivation, you could continue to include the possibly used virtualization layer (XEN, QEMU/KVM, whatever) and finally the hardware design.
Of course, in theory there might be some kernel bug such that e.g. a read() sometimes changes files on disk, but I guess this is outside the scope of that proof system. Only the blog program itself was proven, assuming that the remaining system software as well as hardware are working in a sane way.
If you want your proofs to include the whole operating system, you'd first have to reduce the kernel to a minimal operating system (e.g. MirageOS). If have lots of time, money and motivation, you could continue to include the possibly used virtualization layer (XEN, QEMU/KVM, whatever) and finally the hardware design.
Without reading the sourcecode/proof (bookmarked for later) my guess is that it simply means something along the lines of "the user cannot execute code a la eval". So basically the user can do exactly the specified actions and nothing more.
By "system call", we do not mean "kernel call" but more "call to the system" in a broader sense, that is from the program to its environment (it could be the OS or other libraries). We should probably use another word since this is confusing.
More exactly, we check that the only calls when the user is not logged in are: ReadFile, ListPosts or Log: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...
More exactly, we check that the only calls when the user is not logged in are: ReadFile, ListPosts or Log: https://github.com/clarus/coq-chick-blog/blob/master/Spec.v#...
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 Art of Electronics, but for formal proofs.
Software Foundations
http://www.cis.upenn.edu/~bcpierce/sf/current/index.html
To my knowledge it's the most accessible book/class/tutorial on Coq. Starts off slowly and has a lot of interactive examples. Suitable for self-study. Comparing with what else is out there, really shows how refined and well-tested it is.
Highly recommend.
To my knowledge it's the most accessible book/class/tutorial on Coq. Starts off slowly and has a lot of interactive examples. Suitable for self-study. Comparing with what else is out there, really shows how refined and well-tested it is.
Highly recommend.
Winner winner chicken dinner.
I read the preface and this sounds exactly like what I was looking for. Many thanks!
I read the preface and this sounds exactly like what I was looking for. Many thanks!
I worked through it last year and had a great time. Enjoy!
I've heard good things about Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/).
"This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation."
Edit: There's some comparison of CPDT and SF here: https://lobste.rs/s/c3lj14/certified_programming_with_depend....
"This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation."
Edit: There's some comparison of CPDT and SF here: https://lobste.rs/s/c3lj14/certified_programming_with_depend....
I could recommend Coq Art: http://www.labri.fr/perso/casteran/CoqArt/ Unfortunately, formal proofs are very theoretical and there's a lot of concepts to learn that aren't found in regular programming. This book eases you into things though.
This is great, as more real life examples are needed.
disclaimer: outside of a quick understanding of what "formal proof system" is, I have no deep understanding of how it works.
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 ?
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 ?
It's definitely possible. The hand wavy version is that basically you just throw out all the fancy types, throw out all the proofs, and just leave the data and functions.
So let's say in Coq I write a sorting function. In Coq it could have a type where it takes a list and returns the same list sorted (i.e. proven that it works). I can extract to OCaml and be just left with a function which a type that takes a list and returns a list. However the computation being done is still the same.
The target language doesn't even need types. I don't know if it's still maintained but there used to be an extraction back-end to Scheme (also one for Haskell).
Being a functional language makes things much easier. Need to have something to map algebraic data types, functions, and function application.
So let's say in Coq I write a sorting function. In Coq it could have a type where it takes a list and returns the same list sorted (i.e. proven that it works). I can extract to OCaml and be just left with a function which a type that takes a list and returns a list. However the computation being done is still the same.
The target language doesn't even need types. I don't know if it's still maintained but there used to be an extraction back-end to Scheme (also one for Haskell).
Being a functional language makes things much easier. Need to have something to map algebraic data types, functions, and function application.
My understanding is that, after translation, Agda's Haskell makes rather liberal use of unsafeCoerce :: a -> b (it's already been type checked by Agda, after all).
Yes, that's true for Coq extraction also. You can choose to extract to ML, Haskell or Scheme, but whichever one you pick the target language is basically treated as an untyped language. (Of course, it tries to avoid unsafeCoerce/Obj.magic if possible; if the program can be typed with just simple types, the extracted code should not have any unsafe coercions in it.)
Coq is essentially a verification system and functional programming language all in one. The functional programming language that the proofs are based on has similar (identical in some places) semantics to OCaml. Remaining faithful to these semantics, especially in a verifiable way, quickly becomes herculean. Even formalizing the semantics of a language is a process that takes months.
I understand better, so basically before doing anything you will first need to define what each "part" of the language "means" in term of "logical operation" (like what does the dot operator '.' means in PHP, which type it accepts and it transforms them etc) Right ?
Coq itself is already a programming language, but pure in the sense there cannot be any side effects (like IOs). For this pure part there are already an interpreter and a compiler to OCaml, Haskell or Scheme.
To extend Coq with IOs you need to define each new external call. This is basically what is done in the files https://github.com/clarus/coq-chick-blog/blob/master/Computa... and https://github.com/clarus/coq-chick-blog/blob/master/Extract...
To extend Coq with IOs you need to define each new external call. This is basically what is done in the files https://github.com/clarus/coq-chick-blog/blob/master/Computa... and https://github.com/clarus/coq-chick-blog/blob/master/Extract...
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.
The "finite time" requirement isn't actually related to performance, it's needed to make sure we can prove meaningful things about the return value. If a function never returns a value (or it "returns after an infinite amount of time") then anything we say about its return value will be a counterfactual, and open to all kinds of paradoxes and inconsistencies.
If we want to enforce some actual performance metric, we can use something like cost semantics ( http://lambda-the-ultimate.org/node/5021 ) to enforce complexity bounds (eg. the "big-O" behaviour), then use a few small-scale tests to relate the constant factors in the model to real world values.
If we want to enforce some actual performance metric, we can use something like cost semantics ( http://lambda-the-ultimate.org/node/5021 ) to enforce complexity bounds (eg. the "big-O" behaviour), then use a few small-scale tests to relate the constant factors in the model to real world values.
There's no reason a proof has to take any time - propositions as types is a tool to guide us to correct information flow, it doesn't mean we literally run the proof at every step. If we trust the core, we can erase the proof checking at the point of compilation and we're left with identical machine code that has been proven to do exactly what we expect and specify.
I think he was referring to the fact that the request completes in finite time isn't a tight enough bound.
This is such a terribly badly named language for anyone in the UK!
The name has an history, but the fact that UK (and US) have a problem with it is probably the very reason why it's been kept like this.
After all "bit" in french has exactly the same meaning as "cock" in english. french devs deal with it. I guess it's some kind or revenge...
We actually joke about it! Take a 'bitfield' for example, in french it becomes a 'field of cocks' :)
I'm pretty sure I remember hearing fairly direct word-of-mouth confirmation that the double meaning was completely deliberate.
It's not just that "Coq" might sound like "cock", but a "Coq blog" just sounds even funnier...
I just hate to think of the poor girl/woman who decides she loves the framework...
Why does it have to be a girl/woman? Why would it be any different for a boy/man to say they love Coq?
This actually happened to me. A classmate said something about Coq, and I did a double take. He explained it was a language, but for a second he got my hopes up.
This actually happened to me. A classmate said something about Coq, and I did a double take. He explained it was a language, but for a second he got my hopes up.
I've been told that the French OCaml crowd have (or had) a habit of naming projects after animals. In this case, cockerel.
Coq means rooster (US or cock/cockerel in the UK) and is a symbol of France maybe this has something to do w/ it.
Also, after "Calculus of Constructions" being shortened to "CoC", and then punned with its inventor's name "Coquand".
In one of William Gibson's books (the first trilogy I believe), there was this idea of companies running algorithms on new product names to check if translated in other languages, the name would mean something NSFW. Just imagine how limiting that would be for marketing people, with so many existing human languages.
How does Coq ensure that the request completes in finite time?