# [isabelle] Automation is awesome; one bibliography leads to another

`This comment falls under the "Dude, this is awesome" category, and no
``reply is needed. I try to keep my comments to a minimum, but I make this
``one.
`

`Bibliographies leading to bibliographies led me to Blanchett's
``"Automatic Proofs and Refutations for Higher-Order Logic"
``<http://www4.in.tum.de/%7Eblanchet/>.
`

`There are developers of other provers who listen in, so this comment
``could also serve as a feature request from one user, me, for their products.
`

`I've said that I don't care about automatic proving. For my purposes,
``whatever I prove I have to understand, so automatic proving doesn't help
``me unless I can be shown the automatic prover's proof, and understand
``the details, or have a general idea of what the prover did. My intended
``audience, by and large, also won't be impressed by automatic proofs.
``There has to be educational content in the details of my proofs, where
``the amount of detail has to be balanced (which, of course, requires some
``auto proving), but where there isn't a total absence of details.
`

`On the other hand, as to counterexamples, there's no requirement that I
``understand anything other than that the counterexample has proven me
``wrong, so I'll be keeping in mind the Isabelle tools that will look for
``counterexamples. As Blanchett says,
`

` Novices and experts alike can enter invalid formulas and find
``themselves wasting hours
`` (or days) on an impossible proof; once they identify and correct
``the error, the proof is often easy.
`

`I saw in the past a little of the results of Quickcheck, but I had
``forgotten about the counterexample tools.
`

`But back to automatic proving, I'm sure it'll come in handy when I have
``"The Important Promising Conjecture", or even under less important
``circumstances. What I think I don't want, I sometimes do want.
`

`Power is whatever you need. I had a mini-debate with someone who had no
``sympathy with the idea that I needed a proof assistant instead of an
``automatic prover. Power to him was automatic proving. Power to me was
``being able to specify the proof steps. I guess both are powerful, since
``both take a massive amount of work to implement.
`
--GB

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