Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Comparing Coq and K

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Comparing Coq and K


Chronological Thread 
  • From: Bas Spitters <b.a.w.spitters AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Cc: "grigore.rosu AT runtimeverification.com" <grigore.rosu AT runtimeverification.com>
  • Subject: Re: [Coq-Club] Comparing Coq and K
  • Date: Thu, 6 Feb 2020 22:38:18 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f43.google.com
  • Ironport-phdr: 9a23:Kb6kGxQzJuEzS3kw03B3hiM7pdpsv+yvbD5Q0YIujvd0So/mwa6zYRGN2/xhgRfzUJnB7Loc0qyK6vymBDdLuMre+DBaKdoQDkRD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrs+xxfTonZFdetayX5nKF+Rgh3w4tu88IN5/ylfpv4s+dRMXbnmc6g9ULdVECkoP2cp6cPxqBLNVxGP5nwSUmUXlhpHHQ3I5wzkU5nyryX3qPNz1DGVMsPqQ780Xy+i77pwRx/zlCgHLT85/3rJhcF2kalWvQiupx17w47TfYGVKP9zdb7TcN8GWWZMWNtaWjdfCY2gcYQAE+sBPf5Zr4bjoVsOsQC+DhSoCO/21zNEmmP60ag83u88Ew/JwRYgEsoBv3Tartr7NKkcX+OowqfW0TrNYOhb2Svk6IXSbhwtve2AULB2fMHMyUcvDQTFjlCIpIH4JTyVzfkGvXWD7+phSeKvl3AoqxtqojOywcojkZPFiZgPxlHK7yl52541JdykSE5nf9GkCoBQujqVN4tzWMwiQmVotDwmxb0BvJ62ZS4Hw4kpyR7YbvyIaYmI4hT7WeaKIDd4i2pleLaliBa060Sgzff8Vsas3FdFtCVFjNjMuW4X1xzX9MeHUPx9/0e71TaIzQDT5flIIV0slaXFLZ4hxKQ8mYQOvkTeBiP2glj2jKmKdkUl/+in9frnbav8pp+dOY90ix3xPb4ymsy+BuQ4NBICUHSc+eS50rDo4E73QK1Sg/EojqXUtIrWKMcbq6KjHgNY05sv5wywAjqo1tkTgGMJI0hfeB2diojkI1HOL+78Dfe4m1mslS1kx/HCPrH4ApTMIGXPnK7vfbty5UNQ0gUzzddY55JbDrEOPuj/VVP2tNzdFhM5Mgq0zPj7CNhlyI8SRWaCDrWaPa7Sq1OE++MiL/SWaIIatjvxM/0l6OTvjX89l18dZ66p3Z4PZX+jBPhpOV+VYHT2jtcaCWcKvxY+TPD0h12YSj5efHmyX6cm6TE6DIKqF5vMRoeogLCZxie0AoVWZnxaClCLCXrna4KEW+4VZC2OJs9hjycLWKO6S44h0BGurBX1x6BmLurS4C0YtIjs2MJ75+3JxlkO8mlfCN3V+GWQRSkglWQRAjQywapXoEpny17F37Iu0NJCEtkGzfpSGjwiNILAwvZhQ4T4HAuHYZGSUFe6Xti8Ghk+S9swx5kFZEMrSIbqtQzKwyf/W+xdrLeMHpFht/uEhyGgdfY48G7P0ewat3djR8JOMWO8gasmrlrcAofIlwOSkKP4LP1Bjh6Iz3+KyC+1hG8dUAN0Vv+YD3UWZ0+TvMugo02eFPmhDrMoNgYHwsmHePMTNo/ZyG5eTfKmA+zwJnqrkj7pVxmNz7KIKoHtfjdF0Q==

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



Archive powered by MHonArc 2.6.18.

Top of Page