Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A blog engine written and proven in Coq

coq-blog.clarus.me

Post reply on HN
Print view View original

11–20 of 60 posts

Re: A blog engine written and proven in Coq

#11

Post by pja »

__alexs wrote: post #10
pja wrote: post #3

Earlier quoted context omitted.

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?

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

Re: A blog engine written and proven in Coq

#13

Post by brudgers »

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.

Re: A blog engine written and proven in Coq

#15

Post by hme »

teddyuk wrote: post #12

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

Re: A blog engine written and proven in Coq

#16

Post by djcoin »

amirmc wrote: post #14
teddyuk wrote: post #12

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

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.

Re: A blog engine written and proven in Coq

#17

Post by eli_gottlieb »

wk_end wrote: post #7
wereHamster wrote: post #2

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

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.

Re: A blog engine written and proven in Coq

#18

Post by seanwilson »

wereHamster wrote: post #2

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

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.

Re: A blog engine written and proven in Coq

#19

Post by tpaksoy »

hme wrote: post #15
teddyuk wrote: post #12

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

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