To help students with acquiring the skill of giving mathematical proofs, we developed the educational software Waterproof, which consists of a Rocq plugin and an extension for Visual Studio Code. Waterproof uses controlled natural language, and we try to bring writing proofs in Waterproof as close as possible to writing proofs on paper. In this talk I will discuss some of our design choices, some of the evaluations we have performed, and some preliminary work on using large language models to guide students through exercises.