> Matthew Doty wrote:
> >This isn't *classical logic*, though. It's a sublogic called *intuitionistic logic*.
> I'd disagree slightly.
I'm not trying to say one is right and the other is wrong! These are just the names I learned for them in school.
Intuitionistic logic is great for programming. Haskell is intimately connected to intuitionistic logic.
**Puzzle**: How do you write a type for \\(\bot\\) in Haskell, and then write a program `hilbertExplosion :: _|_ -> a`? (Hint: you might want `{-# LANGUAGE Rank2Types #-}`)
Here's an amazing example of applying Intuitionistic logic to Haskell: two months ago I saw a new compiler plugin released [*JustDoIt*](https://github.com/nomeata/ghc-justdoit):
{-# OPTIONS_GHC -fplugin=GHC.JustDoIt.Plugin #-}
module Test where
import GHC.JustDoIt
foo :: ((a -> r) -> r) -> (a -> ((b -> r) -> r)) -> ((b -> r) -> r)
foo = (…)
It takes the type signature of the program you want, and treats it like a proposition. It then uses an old theorem prover Roy Dykhoff wrote in 1991. Roy based his prover on Gentzen's LJ sequent calculus. It then turns the proof into a program and writes it for you. Still feels like witchcraft...
But... I do a lot of computer proofs. Those are hard. I use the excluded middle *a lot*. You can call me a *tertium non datur* junky. Or just intellectually lazy.