Djinn 是一个定理证明者。您的问题似乎是：定理证明与编程有什么关系？
强类型编程与逻辑有着非常密切的关系。特别是，ML 传统中的传统函数式语言与Intuitionist Propositional Logic密切相关。
口号是“程序就是证明，程序证明的命题就是它的类型”。
一般来说你可以想到
foo :: Foo
话说那foo是一个公式的证明Foo。例如类型
a -> b
对应于函数 from ato b，所以如果你有一个证明a和一个证明a -> b你就有一个证明b。因此，函数完全对应于逻辑中的含义。相似地
(a,b)
对应于合取（逻辑与）。所以逻辑重言式a -> b -> a & b对应于 Haskell 类型 a -> b -> (a,b)
并有证明：
\a b -> (a,b)
这是“和引入规则”，fst :: (a,b) -> a而snd :: (a,b) -> b与2“和消除规则”相对应
同样，a OR b对应于 Haskell 类型Either a b。
在Haskell Curry和William Alvin Howard之后，这种对应有时被称为“Curry-Howard 同构”或“ Curry-Howard 对应”
这个故事因 Haskell 中的非全面性而变得复杂。
Djinn“只是”一个定理证明者。
如果您有兴趣尝试编写克隆，“Simple Theorem Prover”的谷歌搜索结果的第一页有这篇论文，它描述了为 LK 编写一个似乎是用 SML 编写的定理证明器。
编辑：至于“如何证明定理是可能的？” 答案是从某种意义上说并不难。这只是一个搜索问题：
考虑将问题重述为：我们有一组我们知道如何证明 S 的命题，以及一个我们想证明 P 的命题。我们该怎么办？首先，我们问：我们是否已经在 S 中证明了 P？如果是，我们可以使用它，如果不是，我们可以在 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)
如果这些都不起作用
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)
真正的定理证明者有一些聪明，但想法是一样的。“决策程序”的研究领域研究了为某些保证有效的公式寻找证据的策略。另一方面，“战术”着眼于如何以最佳方式对证明搜索进行排序。
至于：“如何将证明翻译成 Haskell？”
形式系统中的每条推理规则都对应着一些简单的 Haskell 构造，所以如果你有一棵推理规则树，你就可以构造一个对应的程序——Haskell 毕竟是一种证明语言。
含义介绍：
\s -> ?
或介绍
Left
Right
和介绍
\a b -> (a,b)
和消除
fst
snd
ETC
augustss 在他的回答中说，他们在 Djinn 中实现这一点的方式对于 SO 的回答来说有点乏味。不过我敢打赌，您可以自己弄清楚如何实现它。