Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Isabelle is actually a "logical framework", so it supports intuitionistic logic, actually its meta theory is intuitionistic higher-order logic.

So this is not because of the logic, it is because of the mindset. Intuitionistic logic is usually championed by people who want to emphasise computation over reasoning, and that is why they build computation as one their reasoning steps into their kernel. They don't have to do that. They do it deliberately, because it aligns with what they like, and how they like to think about logic.



Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: