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