Home

Milawa on Jitawa: a Verified Theorem Prover

Milawa

Aug 2010 - May 2011. Magnus Myreen has developed a verified Lisp system, named Jitawa, which can run Milawa. Our paper about this project was accepted to ITP 2011.

This is pretty interesting: Milawa was already "self-verifying," in the sense explained on the page. More recently, it's been made to run on a verified Lisp runtime, so that means the entire stack down to the X86_64 machine code is verified. Milawa itself is "ACL2-like," so it's not as interesting logically as, say, Isabelle or Coq, but it's far from a toy. Also, the Jitawa formalization apparently took place in HOL4, so you need to trust HOL4. Since HOL4 is an "LCF-like" system, you can do that to the extent that you trust the LCF process, but it doesn't satisfy the de Bruijn criterion in the same way Milawa or Coq do. Nevertheless, this seems like an important step toward the ultimate goal of having a stack that is verified "all the way down," as it were.

By Paul Snively at 2012-02-29 18:34 | Functional | Lambda Calculus | Logic/Declarative | other blogs | 10498 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

xref

Previous mention, about two years ago.

By el-vadimo at Wed, 2012-02-29 19:57 | login or register to post comments

HOL4 and the de Bruijn criterion

HOL had proof-logging and checking in the early 90s, thanks to work by Wai Wong (see this paper). That code is no longer part of the system, but the development version of HOL4 (see github) now has support for the OpenTheory logging/checking system. In between times, Sebastian Skallberg also wrote logging code for HOL4 that was used to transport HOL4 proofs to Isabelle/HOL. The latter is not a small system, but it’s further proof of independent “checkability”.

By michaeln at Wed, 2012-02-29 22:34 | login or register to post comments