在Rust中重新实现Mizar
摘要：一种新的开源证明处理工具mizar-rs的描述，它是Mizar证明系统核心部分的整体重实现，用Rust语言编写。具体而言，实现了Mizar的“检查器”和“分析器”，这两者共同构成Mizar的可信核心。据我们所知，这是第一个也是唯一一个对这些组件进行外部实现的工具。由于Mizar的传递性松散耦合，可以将检查器作为原始检查器的即插即用替代品，并且我们已经成功使用它在8个核心上以11.8分钟的速度对整个MML进行验证，相比原始的Pascal实现，提速了4.8倍。由于Mizar并不是为了有一个小的可信核心而设计，因此检查Mizar证明意味着紧跟着Mizar的步伐，所以我们检测错误的能力有限。尽管如此，我们能够发现多个内存错误，四个原始版本中的完整性错误（在MML中没有被利用），以及一个在46篇不同的MML文章中被利用的非关键性错误。我们希望将这个检查器作为证明导出工具的基础，同时恢复语言的开发。
作者：Mario Carneiro
论文ID：2304.08391
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-04-18