User loginNavigation |
Milawa on Jitawa: a Verified Theorem Prover
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 | 10561 reads
|
Browse archives
Active forum topics |
Recent comments
35 weeks 1 day ago
35 weeks 1 day ago
35 weeks 1 day ago
1 year 5 weeks ago
1 year 9 weeks ago
1 year 11 weeks ago
1 year 11 weeks ago
1 year 13 weeks ago
1 year 18 weeks ago
1 year 18 weeks ago