functional-programming - 如何将经典的自然演绎证明转化为计算机程序？

Question

我一直在学习命题逻辑的自然演绎（特别是 Chiswell 和 Hodges 的数学逻辑教科书第 2 章中描述的系统），并且一直在探索 Curry-Howard 对应关系。这展示了如何进行自然演绎推导并相当直接地转换为使用 Scala 或 Haskell 等语言的类型化程序。或者至少，对于不使用“Reducio ad absurdum”（RAA）规则的直觉证明，我可以。通过一些阅读，我发现也有一些方法可以探索经典证明的计算解释，也许使用控制运算符，如call/cc. 是否可以在真正的编程语言中使用这些想法？希望有人可以给出一些关于这可能如何工作的指示/示例。