2

我看到很多关于如何使用 ACL2 来证明代码的资源，正如您所期望的那样，但没有关于如何在生产中使用您的证明代码的资源。

我是否可以调整我的 ACL2 代码以使用 CLISP/Scheme/Clojure？ACL2 也可以运行我的代码吗？（教程在哪里，我使用 ACL2 不是按照它的目的吗？）

谢谢！

4

0 回答 0