> 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.