2 ms·
curious why you referred specifically on isabelle, which looks ancient and over engineered, there are many other tools and langs in this area. I am not critici
by riku_iki 3y ago
curious why you referred specifically on isabelle, which looks ancient and over engineered, there are many other tools and langs in this area.
I am not criticizing, but curious about your opinion.
- c-cube 3y agoIsabelle is good at counter examples in ways few other proof assistants are. In general its automation is excellent, partly because it uses a less powerful logic (HOL instead of CIC; more expressive logics are harder to write automation for). It's not obsolete.