12
$\begingroup$

Has there been notable research or attempts to integrate a JIT compiler into a proof assistant in order to achieve performance gains for proof verification, or general programming?

Whilst it may seem like doing so increases the risk of letting incorrect proofs through in complicated JIT implementations, perhaps there's value in faster feedback, with a slower more careful pass always something that could be done later.

What is known about the intersection between these spaces?

$\endgroup$
2
  • $\begingroup$ IIRC Lean has this for tactics $\endgroup$
    – ice1000
    Feb 9, 2022 at 3:04
  • $\begingroup$ Idk if Coq native_compute counts $\endgroup$
    – ice1000
    Feb 9, 2022 at 3:04

2 Answers 2

10
$\begingroup$

Apart from the well-known native_compute feature of Coq, I'd like to share two JITted dependently-typed programming languages which are used for theorem proving:

  • Lean 4: in this WITS talk, Seb said that for files that are not actively edited, the tactics within are compiled to dynamic-linked-libraries, and loaded into the compiler, and then executed. I believe this is in some sense a JIT compilation.

  • mlang: they elaborate the surface syntax and compile to HOAS, where binding structures are turned into JVM bytecode (see PlatformEvaluator.platformEval). Andras Kovacs said it's supposed to be "always faster". Unlike Lean 4 who JITs only tactics, mlang JITs all bindings.

$\endgroup$
0
7
$\begingroup$

Coq's native_compute will invoke a modified version of ocamlc to just-in-time compile code for native evaluation. Similarly, vm_compute JITs code to be run by a bytecode interpreter. Both of these are for performance, though often the overhead of compiling to native code dwarfs the time spent running, to the point that native_compute is often slower than vm_compute.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.