A blog engine written and proven in Coq

http://coq-blog.clarus.me/a-blog-engine-written-and-proven-in-coq.html

by jcurbo • 11 years ago

185 58 11 years ago

coq-blog.clarus.me

wereHamster• 11 years ago

The purity of Coq ensures that each request is answered exactly once in finite time.

How does Coq ensure that the request completes in finite time?

pja2• 11 years ago

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.

__alexs• 11 years ago

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?

wk_end• 11 years ago

Coq isn't Turing complete - it has a termination checker that needs to be able to determine that your functions terminate.

eli_gottlieb4• 11 years ago

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.

seanwilson4• 11 years ago

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.

more_original4• 11 years ago

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.

pjmlp• 11 years ago

This is great, as more real life examples are needed.

hrjet• 11 years ago

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?

vog• 11 years ago

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.

kriro• 11 years ago

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.

clarus4• 11 years ago

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

legulere• 11 years ago

Is it also proven that no cross-site-scripting attacks are possible?

clarus4• 11 years ago

No, nothing is done about it, the post contents are not even escaped to generate safe HTML.

teddyuk• 11 years ago

This is such a terribly badly named language for anyone in the UK!

amirmc• 11 years ago

I've been told that the French OCaml crowd have (or had) a habit of naming projects after animals. In this case, cockerel.

djcoin• 11 years ago

Coq means rooster (US or cock/cockerel in the UK) and is a symbol of France maybe this has something to do w/ it.

hme• 11 years ago

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

tpaksoy• 11 years ago

It's not just that "Coq" might sound like "cock", but a "Coq blog" just sounds even funnier...

leoc2• 11 years ago

I'm pretty sure I remember hearing fairly direct word-of-mouth confirmation that the double meaning was completely deliberate.

jeremiep• 11 years ago

We actually joke about it! Take a 'bitfield' for example, in french it becomes a 'field of cocks' :)

lispm• 11 years ago

Maybe the UK should get familiar with the idea that they are not the center of the world?

bshimmin• 11 years ago

You mean "centre", right?

omega_rythm• 11 years ago

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.

brudgers• 11 years ago

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.

leoc2• 11 years ago

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

chriswarbo3• 11 years ago

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 ;)

mcmancini2• 11 years ago

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.

seanwilson4• 11 years ago

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.

adultSwim2• 11 years ago

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.

mcmancini2• 11 years ago

Winner winner chicken dinner.

I read the preface and this sounds exactly like what I was looking for. Many thanks!

pseudonom-2• 11 years ago

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

allan_s2• 11 years ago

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 ?

sun_machine• 11 years ago

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.

allan_s2• 11 years ago

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 ?

adultSwim2• 11 years ago

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.

pseudonom-2• 11 years ago

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

skybrian• 11 years ago

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.

ocharles• 11 years ago

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.

CompleteSkeptic• 11 years ago

I think he was referring to the fact that the request completes in finite time isn't a tight enough bound.

chriswarbo3• 11 years ago

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.

A blog engine written and proven in Coq

Related Stories