While I don’t understand much algebra, I know Isabelle and implemented a checker in Isabelle/HOL. I used the Refinement Framework and Sepref to generated code in Standard ML. The code is mostly functional (except for the hashmap that is synthesized automatically by Sepref – no need to understand and know anything about it!).

How does Pastèque work? I started with an abstract calculus that models the rules of the proofs system. Then I make the calculus more concrete, e.g., with lists to represent polynomials. Finally, I make everything executable.

Now, you might wonder why I did not target LLVM using the Isabelle-LLVM. Well, we need arbitrary large integers and there is no binding from Isabelle-LLVM to GMP and no hand-written library for it.