# Re: [isabelle] Theorem-proving for a Bayesian model compiler

On Tue, 15 Mar 2011, Kevin Van Horn wrote:

`* Ability to call the theorem prover as a software module in a larger
``system (no user interaction). This would be for tasks simple enough to
``fully automate with appropriate tactics, or to spit out subgoals for
``which the user will need to provide proofs in harder cases.
`

`It is not as simple as I would like it to have, but it works, and people
``have done it before, e.g. in the Isabelle/TLA+ IDE. (The technology for
``Isabelle integration is about to change substantially in the coming
``years.)
`

`How does Isabelle rate on these? Would a different theorem prover /
``proof assistant better fill these requirements?
`

`(BTW I'm also looking at HOL Light and HOL 4, which appear have the last
``three features above, but my impression is that Isabelle is easier to
``use for interactive proof and that the finished proofs are easier to
``read.)
`

`The HOL systems are not fundamentally different. There is mainly a
``tendency towards more frugal system infrastructure -- HOL Light is
``especially minimalistic.
`

`The main alternative to Isabelle is actually Coq, but there are quite
``different logical foundations, and less system manuals.
`
Makarius

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