I also experimented with Isabelle since it had a formalisation of conduction. The interface has improved massively since then, with a much more intuitive "assuming X then Y follows by Z" kind of syntax which Xin was exploiting (I don't honestly think he had much understanding of the details of Isabelle - Z was generally blast (one of the built-in automated reasoning algorithms).
Larry handed over most of the development of Isabelle to Tobias Nipkow while I was still in Edinburgh (or possibly Tobias just gradually took it on - certainly by the turn of the century I'd say Tobias was clearly driving much of the development). I'm not sure who is running it now, digging around the details of Isabelle 2024, suggests Larry and Tobias are still overall in charge but most of the development work is being done by others and there is some organisation called Isabelle CTO that seems to coordinate this in some way.
no subject
Larry handed over most of the development of Isabelle to Tobias Nipkow while I was still in Edinburgh (or possibly Tobias just gradually took it on - certainly by the turn of the century I'd say Tobias was clearly driving much of the development). I'm not sure who is running it now, digging around the details of Isabelle 2024, suggests Larry and Tobias are still overall in charge but most of the development work is being done by others and there is some organisation called Isabelle CTO that seems to coordinate this in some way.