Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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?
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.
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.
