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 "simple".

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 MHonArc.