It is fairly easy to get basic support for Proof General for HOL, and this has recently been tried for HOL 98. However, it would be a bigger and more interesting project to get proper and complete support for HOL working. There are a couple of problems unique to HOL.
Much more than Isabelle, HOL relies on its meta language, ML. HOL proof scripts often use batch-oriented single step tactic proofs constructed in ML, but Proof General does not offer an easy way to edit these kind of proofs (as opposed to multi-step interactive proofs). The Boomburg-HOL Emacs interface by Koichi Takahashi and Masima Hagiya addressed this problem, as well as providing support for proof-by-pointing to HOL. Their interface could perhaps be reinterpreted or reimplemented inside Proof General. Implemented in a generic way, batch script editing would also be useful for Isabelle.
Another problem is that HOL scripts sometimes use SML structures, which can cause confusion because Proof General does not really parse SML, it just looks for semicolons. This could be improved by taking a better parser (e.g. from sml mode).
Finally, to fully support the current Proof General feature set, it would be useful to extend HOL with support for communicating file-dependency information to Proof General, and term-structure markup for proof by pointing.
Skills: Some Standard ML, some Emacs Lisp. Basic understanding of proof assistant behaviour, interest in HOL.
Proposer: David Aspinall.