Re: [isabelle] Theorem-proving for a Bayesian model compiler
On Wed, 16 Mar 2011, Lawrence Paulson wrote:
Mike Gordon has a snappy description of the differences between the
systems: Isabelle provide a better out-of-the-box experience, while HOL
is better as an API for writing code that performs inference.
The various versions of HOL are much simpler internally than Isabelle,
which simplifies programming.
Lets say these systems are closer to the bare metal, so it is easier to
read through the full sources and get an impression how it works.
In contrast, Isabelle is more like a Linux kernel over the bare logic, so
you need to understand some higher structuring principles. I would
nonetheless call it simple, in the same way a modern operating system is
BTW, the APIs of Isabelle have been cleaned up a lot in recent years, so
the simplicity is now easier to see, without the historical baggage
getting in the way.
This archive was generated by a fusion of
Pipermail (Mailman edition) and