<p>Djinn is a theorem prover.  It seems your question is: what does theorem proving have to do with programming?</p>

<p>Strongly typed programming has a very close relationship to logic.  In particular, traditional functional languages in the ML tradition are closely related to <a href="http://en.wikipedia.org/wiki/Intuitionistic_logic">Intuitionist</a> <a href="http://en.wikipedia.org/wiki/Propositional_calculus">Propositional Logic</a>.  </p>

<p>The slogan is "programs are proofs, the proposition that a program proves is its type."<br>
In general you can think of</p>

<pre><code> foo :: Foo
</code></pre>

<p>as saying that <code>foo</code> is a proof of the formula <code>Foo</code>.  For example the type</p>

<pre><code> a -&gt; b  
</code></pre>

<p>corresponds to functions from <code>a</code> to <code>b</code>, so if you have a proof of <code>a</code> and a proof of <code>a -&gt; b</code> you have a proof of <code>b</code>.  So, function correspond perfectly to implication in logic.  Similarly</p>

<pre><code>(a,b)
</code></pre>

<p>Corresponds to conjunction (logic and). So the logic tautology <code>a -&gt; b -&gt; a &amp; b</code> corresponds to the Haskell type  <code>a -&gt; b -&gt; (a,b)</code>
and has the proof:</p>

<pre><code>\a b -&gt; (a,b)
</code></pre>

<p>this is the "and introduction rule"
While, <code>fst :: (a,b) -&gt; a</code> and <code>snd :: (a,b) -&gt; b</code> correspond to the 2 "and elimination rules"</p>

<p>similarly, <code>a OR b</code> corresponds to the Haskell type <code>Either a b</code>.</p>

<p>This correspondence is sometimes referred to as the "Curry-Howard Isomorphism" or "<a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard Correspondence</a>" after <a href="http://en.wikipedia.org/wiki/Haskell_Curry">Haskell Curry</a> and <a href="http://en.wikipedia.org/wiki/William_Alvin_Howard">William Alvin Howard</a></p>

<p>This story is complicated by non-totality in Haskell.</p>

<p>Djinn is "just" a theorem prover.  </p>

<p>If you are interested in trying to write a clone, the first page of google results for "Simple Theorem Prover" has <a href="http://arxiv.org/pdf/cs.LO/9301110.pdf">this</a> paper which describes writing a theorem prover for LK that appears to be written in SML.  </p>

<p>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:</p>

<p>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 <em>pattern match</em> on P</p>

<pre><code>case P of
   (a -&gt; b) -&gt; add a to S, and prove b (-&gt; introduction)
   (a ^ b)  -&gt; prove a, then prove b (and introduction)
   (a v b)  -&gt; try to prove a, if that doesn't work prove b (or introduction)
</code></pre>

<p>if none of those work</p>

<pre><code>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 -&gt; P) ^ (b -&gt; P)` (or elimination)
for each implication `a -&gt; P` is S, try proving `a` (-&gt; elimination)
</code></pre>

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

<p>As to: "How can proofs be translated into Haskell?"</p>

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

<p>Implication introduction:</p>

<pre><code>\s -&gt; ?
</code></pre>

<p>Or introduction</p>

<pre><code>Left
Right
</code></pre>

<p>And introduction</p>

<pre><code>\a b -&gt; (a,b)
</code></pre>

<p>And elimination</p>

<pre><code>fst
snd
</code></pre>

<p>etc </p>

<p>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.</p>
How does Djinn work?
<p>OK, so I realise that I will probably regret this for the rest of my life, but... How does Djinn actually work?</p>

<p>The documentation says that it uses an algorithm which is "an extension of LJ" and points to a long confusing paper about LJT. As best as I can tell, this is a big complicated system of highly formalised rules for figuring out which logical statements are true or false. But this doesn't even <em>begin</em> to explain how you turn a type signature into an executable expression. Presumably all the complicated formal reasoning is <em>involved</em> somehow, but the picture is crucially incomplete.</p>

<hr/>

<p>It's a bit like that time I tried to write a Pascal interpretter in BASIC. (Don't laugh! I was only twelve...) I spent hours trying to figure it out, and in the end I had to give up. I just couldn't figure out how the heck you get from a giant string containing an entire program, to something you can compare against known program fragments in order to decide what to actually do.</p>

<p>The answer, of course, is that you need to write a thing called a "parser". Once you comprehend what this is and what it does, suddenly everything becomes <em>obvious</em>. Oh, it's still not trivial to code it, but the <em>idea</em> is simple. You just have to write the actual code. If I'd known about parsers when I was twelve, then maybe I wouldn't have spent two hours just staring at a blank screen.</p>

<p>I suspect that what Djinn is doing is fundamentally simple, but I'm missing some important detail which explains how all this complicated logical gymnastics relates to Haskell source code...</p>