The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Hello Brandon,

Thanks for the elaboration.

As part of the comparison with Coq, I would expect a discussion of the
trusted code base. Could you say more about that?
I'd also be interested in a comparison with certicoq, but I'll guess
we'll have to wait for that to be released.

Best regards,

Bas

On Thu, Feb 6, 2020 at 9:10 PM Brandon Moore 
<brandon_m_moore AT yahoo.com>
 wrote:
>
> Hello Bas
>
> For a bit more context, our comparison is specifically focused on defining 
> programming languages and verifying programs written in those languages (as 
> opposed to proving metatheory about the languages). This is what we've been 
> using K for at Runtime Verification, and we been asked how it compares to 
> Coq for that specific purpose. We're comparing K and Coq in the domain that 
> K is designed to address; for more general reasoning like verifying 
> consensus protocols we happily use Coq ourselves. The thing where K is 
> distinctly faster is the performance of executing a program according to a 
> language definition; program verification times were reasonably similar in 
> our tests.
>
> K language definitions are based on a form of rewrite rules, and we support 
> execution with a compiler targeting LLVM.
> Coq supports many styles of defining semantics, but we believe the best 
> execution performance would come from an operational semantics with the 
> transition relation defined by an extractible function. A previous K 
> backend compiled to OCaml, and we only moved to more direct code generation 
> when we couldn't further improve performance there, so we are confident K 
> yields faster results than code extraction Coq. Also, language semantics in 
> Coq seem to quite rarely use an extractible style, instead of inductively 
> defined relations. I agree inductively defined relations are much more 
> convenient for proofs, but it does mean that getting program extraction 
> working requires additional user effort to write an alternative form of the 
> language definition (or to develop a code generator for automatically 
> making the conversion).
>
> As for why we moved away from OCaml, we found that translating a large 
> number of execution rules into a large match statement hit a bad case in 
> its algorithm for compiling matches. A match with many large patterns blows 
> out the cache of previously handled shapes, losing precision and 
> performance of the executable while hurting compile times from touching so 
> much memory. We're actually still building on Luc Maranget's, but using his 
> paper "Compiling Pattern Matching to Good Decision Trees" instead of 
> preferring code size of execution speed with OCaml's backtracking algorithm 
> based on his work with Fabrice Le Fessant in "Optimizing Pattern Matching".
>
> Brandon
> On Monday, February 3, 2020, 12:26:43 PM CST, Bas Spitters 
> <b.a.w.spitters AT gmail.com>
>  wrote:
>
>
> Dear Grigore,
>
> This blog-post caught some attention from Coq-users, who don't fully
> understand how to compare the two systems.
>
> https://runtimeverification.com/blog/k-vs-coq-as-language-verification-frameworks-part-1-of-3/
>
> you later added that K is automatic (not interactive) and faster than Coq.
>
> I'm wondering by what benchmark it is faster than Coq.
>
> Emilio Gallego suggested that K might be a way to address the third
> challenge of the poplmark.
> "Challenge 3: Testing and Animating with Respect to the Semantics"
> https://blog.sigplan.org/2020/01/29/mechanized-proofs-for-pl-past-present-and-future/
>
> However, I've been unable to find solutions of the poplmark in K.
>
> I've found the following solutions to challenge 3 (but the poplmark
> website seems down).
> https://xavierleroy.org/POPLmark/locally-nameless/
> https://www.seas.upenn.edu/~plclub/poplmark/fairbairn.html
> https://www.seas.upenn.edu/~plclub/poplmark/berghofer.html
> https://www.seas.upenn.edu/~plclub/poplmark/xi.html
>
> Best regards,
>
> Bas