I asked the what is needed to move from design by contract to using a proof assistant?
not realizing that proof assistant seems to imply interactivity. I now realize I meant something else - automated theorem provers - perhaps.
I want to rephrase my question but:
- It would slightly invalidate the answer so far - providing a moving target is not good
also:
- Are questions about automated theorem provers even on topic?
(the help text is still the standard SE one)
Looking at How are we doing in beta? this site appears to be low on traffic and might not make it out of beta (I may have this wrong).
Would it make sense to rescope it to include all manner of tools for assisting with proofs and/or formal methods?
Related I've just asked Does a proof assistant have to be interactive?