Comment

Comment by practal

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.

parent practal 2 months ago

No comments yet

Be the first to share your thoughts.

Live from the official Hacker News API

A modern reader for Hacker News · SvelteKit + Skeleton