21–30 of 60 posts
Earlier quoted context omitted.
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.
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...
> 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…
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.
Earlier quoted context omitted.
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.
[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.]
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.
It's trivial: proof is by EFQ. ;)
Earlier quoted context omitted.
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…
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.
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.
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.
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...