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.
A blog engine written and proven in Coq
41–50 of 60 posts
Re: A blog engine written and proven in Coq
#42This 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.
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.
Re: A blog engine written and proven in Coq
#43Earlier quoted context omitted.
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...
I just hate to think of the poor girl/woman who decides she loves the framework...
Re: A blog engine written and proven in Coq
#44disclaimer: 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…
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.
Re: A blog engine written and proven in Coq
#45This 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.
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.
Re: A blog engine written and proven in Coq
#46This 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.
Re: A blog engine written and proven in Coq
#47Not 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.
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 ;)
Re: A blog engine written and proven in Coq
#48Earlier 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.
Isn't that coinductive recursion?
"corecursion" is usually a recursion that goes via multiple definitions.
Re: A blog engine written and proven in Coq
#49Is 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.
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....
Re: A blog engine written and proven in Coq
#50Earlier quoted context omitted.
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.
Isn't that coinductive recursion? "corecursion" is usually a recursion that goes via multiple definitions.
In the context of Coq, the word "corecursion" is always used for coinductive recursion. I guess a Coq programmer would call what you describe "mutual recursion".