This large-scale research project (with european funding) might make proof assistants, and in particular Isabelle/HOL, more usable for mathematicians. The project plan contains many more details on the expected course of actions. This effort is also a bit unusual in that it will involve mathematicians as much as possible.
I’ve used Isabelle/HOL a bit in the past, and always found it just short of being comfortable enough to me (my background is in math), so it’s exciting to see some effort put towards bridging that comfort gap. As I get older, it’s definitely clear to me that language/tool ergonomics is as important (if not more important) than many of the features I would have prioritized in the past (speed, purity, etc). I’d much rather spend my days writing in a mediocre language that is comfortable to use (good ecosystem + dependency management, clean syntax, etc) than a great language that is uncomfortable to use (Haskell is the shining example here, I love it, but I hate writing it because of how clumsy the tooling is).
Maybe I’m just lazy, but I don’t have the mental horsepower to learn the follies and foibles of most languages these days, so it’s fantastic when I see what I would consider a great tool (Isabelle) undergoing some concerted effort to improve the ergonomics – a bit of ‘have my cake and eat it too’. Rust also recently noted effort going toward that route, another fine language laying just on the other side of comfortable to me; so hopefully these mark a trend towards more comfortable usage.
Sounds like what Focalize project attempted. Originally wanted an IDE and everything.
http://focalize.inria.fr
At this point, I’d say make one that does ACL2, Coq, and Isabelle/HOL. Almost all top-notch verification of software and hardware is done in one of these if we’re just counting FOSS. There was also work by a woman in UK discharging some proof obligations of HOL via automated solvers. There’s also work verifying common structures or functions with reuse potential. Basically, an IDE + more of all that for those three provers would be best investment if talking the heavy kind of verification.
I went through about 40% of Software Foundations with some friends a couple years ago. As someone with a meaningful FP background but not a lot of formal math training, I found it enjoyable, but didn’t find myself reaching for the tool that often. I definitely could see the complexity of setup being a barrier to a working mathematician, and the unfamiliarity of the notation would be a significant issue as well I’m sure.
This looks like a very interesting effort, I hope they make some inroads, bridging the gap here.