Log In

Abstraction Boundaries and Spec Driven Development in Pure Mathematics

Files

S0273-0979-2024-01831-X.pdf (211.71 KB)

Publication date

2024-04

Authors

Commelin, JohanISNI 0000000518030475
Topaz, A

Editors

Advisors

Supervisors

DOI

https://doi.org/10.1090/bull/1831

Document Type

Article

Metadata

Show full item record

Collections

Utrecht University Repository
Open Access logo

License

taverne

Abstract

In this article we discuss how abstraction boundaries can help tame complexity in mathematical research with the help of an interactive theorem prover. While many of the ideas we present here have been used implicitly by mathematicians for some time, we argue that the use of an interactive theorem prover introduces additional qualitative benefits in the implementation of these ideas.

Keywords

Taverne, Applied Mathematics, General Mathematics

Citation

Commelin, J & Topaz, A 2024, 'Abstraction Boundaries and Spec Driven Development in Pure Mathematics', Bulletin of the American Mathematical Society, vol. 61, no. 2, pp. 241-255. https://doi.org/10.1090/bull/1831

URI

https://dspace.library.uu.nl/handle/1874/438473