How do you think the tooling for performing proof engineering compares to all the tooling that exists for software development – code editors and IDE’s, language servers enabling code completion and refactoring, debuggers, etc? Or are they the same tools?
I’m curious if there is a need for better tooling to support this work or if it is similar to software development.
They are overlapping but different. I’ve given a few talks about this over the years, but I don’t think there are any slides public. A lot of the standard software engineering tooling is useful and used (version control, IDEs, code completion etc; we use all of these on a daily basis), but a lot more could be done in proof refactoring, proof repair, proof recommendation. Needs more research, but it’s also a fairly active area of research.