Re: [isabelle] Where to learn about HOL vs FOL?

On Fri, 8 Feb 2013, Freek Wiedijk wrote:

I gather that the Coq kernel also contains a big chunk of
C code. Surprising, to say the least.

Not if you consider Coq to be a functional language that
you want to execute as fast as possible.

This seems to refer to the virtual machine that runs at the bottom of Coq. (We would need some Coq experts here, or move that thread to coq-club, if anybody dares to do it.)

Looking the problem from a higher level, it is the old debate how you make the prover: LCF-style to run through the inference kernel at run-time, or somehow native as part of the computational part of the logic. This also means the logic is made in a way to have a computational part in the first place (like Coq, Agda, etc.).

My impression is that the LCF-style run-time interpretation turns out as surprisingly fast in many practical applications, both relatively and absolutely compared to the Coq computation model. In a system like Isabelle/HOL you are not limited to a single built-in computational model, you can do things with different formal status (say HOL specifications vs. emitted code in other languages). In principle, Coq does not limit you either, but the traditional way is to assimilate everything within its one big formal system.

Incidently, a Coq user has explained to me just last weak, that the notable Isabelle application IsaFoR/CeTA performs best in its category. The code that does the actual work in the end is native in Haskell, without the prover preventing it from being really fast.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.