A blog engine written and proven in Coq
coq-blog.clarus.me
coq-blog.clarus.me
How does Coq ensure that the request completes in 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?
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 :)
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.
[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.]
http://www.cse.chalmers.se/research/group/logic/TypesSS05/Ex...
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?
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.
"corecursion" is usually a recursion that goes via multiple definitions.
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.
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.
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.
But 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. ;)
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 ;)
> 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?
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.
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#...
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.
I read the preface and this sounds exactly like what I was looking for. Many thanks!
"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....
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 ?
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...
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.
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.
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.