Document Open Access Logo

Reimplementing Mizar in Rust

Author Mario Carneiro

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.10.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Mario Carneiro
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

Work supported by the Hoskinson Center for Formal Mathematics at Carnegie Mellon.

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 As Get 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

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)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Mark Miles Adams. Proof auditing formalised mathematics. Journal of Formalized Reasoning, 9(1):3-32, 2016. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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.
  5. Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153-245, 2010. Google Scholar
  6. 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. Google Scholar
  7. Cezary Kaliszyk and Karol Pąk. Semantics of Mizar as an Isabelle object logic. Journal of Automated Reasoning, 63:557-595, 2019. Google Scholar
  8. 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. Google Scholar
  9. Roman Matuszewski and Piotr Rudnicki. Mizar: the first 30 years. Mechanized mathematics and its applications, 4(1):3-24, 2005. Google Scholar
  10. Michal Muzalewski. An outline of PC Mizar. Fondation Philippe le Hodey, 1993. Google Scholar
  11. 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.
  12. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. Journal of Automated Reasoning, 37:21-43, 2006. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact