If you do not know Joy and want to check it out, you will notice that the link in this page is broken. A mirror is available here: http://www.kevinalbrecht.com/code/joy-mirror/index.html
Was recently blown away to find out that propositional logic can be whittled down to just modus ponens and the single axiom:
((((p -> q) -> (~r -> ~s)) -> r) -> t) -> ((t -> p) -> (s -> p))
I would love to combine the above with my interest in rich type systems. Anyone aware of anything that, in spirit, marries Haskell and Factor?