Djinn is a theorem prover. It seems your question is: what does theorem proving have to do with programming?
Strongly typed programming has a very close relationship to logic. In particular, traditional functional languages in the ML tradition are closely related to Intuitionist Propositional Logic.
The slogan is "programs are proofs, the proposition that a program proves is its type."
In general you can think of
foo :: Foo
as saying that foo is a proof of the formula Foo. For example the type
a -> b
corresponds to functions from a to b, so if you have a proof of a and a proof of a -> b you have a proof of b. So, function correspond perfectly to implication in logic. Similarly
(a,b)
Corresponds to conjunction (logic and). So the logic tautology a -> b -> a & b corresponds to the Haskell type a -> b -> (a,b)
and has the proof:
a b -> (a,b)
this is the "and introduction rule"
While, fst :: (a,b) -> a and snd :: (a,b) -> b correspond to the 2 "and elimination rules"
similarly, a OR b corresponds to the Haskell type Either a b.
This correspondence is sometimes referred to as the "Curry-Howard Isomorphism" or "Curry-Howard Correspondence" after Haskell Curry and William Alvin Howard
This story is complicated by non-totality in Haskell.
Djinn is "just" a theorem prover.
If you are interested in trying to write a clone, the first page of google results for "Simple Theorem Prover" has this paper which describes writing a theorem prover for LK that appears to be written in SML.
Edit:
as to "how is theorem proving possible?" The answer is that in some sense it isn't hard. It is just a search problem:
Consider the problem restated as this: we have a set of propositions we know how to prove S, and a proposition we want to prove P. What do we do?
First of all, we ask: do we already have a proof of P in S? If so, we can use that, if not we can pattern match on P
case P of
(a -> b) -> add a to S, and prove b (-> introduction)
(a ^ b) -> prove a, then prove b (and introduction)
(a v b) -> try to prove a, if that doesn't work prove b (or introduction)
if none of those work
for each conjunction `a ^ b` in S, add a and b to S (and elimination)
for each disjunction `a v b` in S, try proving `(a -> P) ^ (b -> P)` (or elimination)
for each implication `a -> P` is S, try proving `a` (-> elimination)
Real theorem provers have some smarts, but the idea is the same. The research area of "Decision Procedures" examines strategy for finding proofs to certain kinds of formula that are guaranteed to work. On the other hand "Tactics" looks at how to optimally order the proof search.
As to: "How can proofs be translated into Haskell?"
Each inference rule in a formal system corresponds to some simple Haskell construct, so if you have a tree of inference rules, you can construct a corresponding program--Haskell is a proof language after all.
Implication introduction:
s -> ?
Or introduction
Left
Right
And introduction
a b -> (a,b)
And elimination
fst
snd
etc
augustss says in his answer that they way he implemented this in Djinn is a little tedious for an SO answer. I bet though, that you can figure it how to implement it on your own.
