The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

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