LIPIcs.ITP.2023.10.pdf
- Filesize: 0.8 MB
- 18 pages
Document
Reimplementing Mizar in Rust
Author
Mario Carneiro 
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
Acknowledgements
I would like to thank Josef Urban and Jeremy Avigad for their support and encouragement, and Adam Naumowicz and SUM for taking the courage to finally open-source Mizar, without which it would not have been possible to publish this paper and accompanying code.
Cite AsGet BibTex
Mario Carneiro. Reimplementing Mizar in Rust. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.10
https://doi.org/10.4230/LIPIcs.ITP.2023.10
Abstract
This paper describes a new open-source proof processing tool, mizar-rs, a wholesale reimplementation of core parts of the Mizar proof system, written in Rust. In particular, the "checker" and "analyzer" of Mizar are implemented, which together form the trusted core of Mizar. This is to our knowledge the first and only external implementation of these components. Thanks to the loose coupling of Mizar’s passes, it is possible to use the checker as a drop-in replacement for the original, and we have used this to verify the entire MML in 11.8 minutes on 8 cores, a 4.8× speedup over the original Pascal implementation. Since Mizar is not designed to have a small trusted core, checking Mizar proofs entails following Mizar closely, so our ability to detect bugs is limited. Nevertheless, we were able to find multiple memory errors, four soundness bugs in the original (which were not being exploited in MML), in addition to one non-critical bug which was being exploited in 46 different MML articles. We hope to use this checker as a base for proof export tooling, as well as revitalizing development of the language.
Subject Classification
ACM Subject Classification
- Mathematics of computing → Mathematical software performance
- Software and its engineering → Formal methods
- Social and professional topics → Systems analysis and design
Keywords
- Mizar
- proof checker
- software
- Rust
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Mark Miles Adams. Proof auditing formalised mathematics. Journal of Formalized Reasoning, 9(1):3-32, 2016.
-
Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61:9-32, 2018.
-
Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Intelligent Computer Mathematics: International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings., pages 261-279. Springer, 2015.
- Mario Carneiro. The Divergence of the Sum of Prime Reciprocals. Formalized Mathematics, 30(3):209-210, 2022. URL: https://doi.org/doi:10.2478/forma-2022-0015.
-
Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153-245, 2010.
-
John Harrison. A Mizar Mode for HOL. In Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, volume 1125 of Lecture Notes in Computer Science, pages 203-220, Turku, Finland, 1996. Springer-Verlag.
-
Cezary Kaliszyk and Karol Pąk. Semantics of Mizar as an Isabelle object logic. Journal of Automated Reasoning, 63:557-595, 2019.
-
Ondřej Kunčar and Andrei Popescu. A consistent foundation for Isabelle/HOL. In Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings 6, pages 234-252. Springer, 2015.
-
Roman Matuszewski and Piotr Rudnicki. Mizar: the first 30 years. Mechanized mathematics and its applications, 4(1):3-24, 2005.
-
Michal Muzalewski. An outline of PC Mizar. Fondation Philippe le Hodey, 1993.
- Josef Urban. XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy. In Michael Kohlhase, editor, Mathematical Knowledge Management, 4th International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised Selected Papers, volume 3863 of Lecture Notes in Computer Science, pages 346-360. Springer, 2005. URL: https://doi.org/10.1007/11618027_23.
-
Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. Journal of Automated Reasoning, 37:21-43, 2006.