Waterproof Editor: an educational environment for proof assistants and programming languages
2026-06-01 • Computers and Society
Computers and Society
AI summaryⓘ
The authors created Waterproof Editor to help teach using proof assistants and programming languages. It builds on previous software called Waterproof that helped students learn how to write mathematical proofs. The new editor includes features like better formatting and clear input areas, which are now available as a reusable software package. The authors encourage others to use and integrate this tool into their educational programs and offer support for doing so.
proof assistantsmathematical proofsprogramming languageseducational softwarenpm packagerich formattingsoftware componentseducational environmentinput areas
Authors
Pim Otte, Dick Arends, Raul Sánchez Flores, Pieter Wils, Jim Portegies
Abstract
Waterproof Editor provides an educational environment specifically targeted to teaching with proof assistants or programming languages. It arose from Waterproof, educational software targeted at helping students acquire the skill of giving mathematical proofs. Its original features such as enabling rich formatting and providing clear input areas are now abstracted away in an npm package and can be used in different educational contexts. We invite interested parties to use this component in their educational software, and offer to assist with this.