Waterproof: educational software for learning how to writ...

Stream: Lean for teaching

[Marcello Seri]

With coq there is also this recent paper/tool that makes it much more student-friendly: https://arxiv.org/abs/2211.13513

[Bulhwi Cha]

Waterproof looks like Lean games.

[Patrick Massot]

Unfortunately this software seems abandoned. It doesn't build (see https://github.com/impermeable/waterproof/issues/82) and most pages of the website are blank, for instance https://impermeable.github.io/src/guide.html. They also don't answer emails.

[Marcello Seri]

That is surprising, the were presenting it just a few weeks ago at the netherlands mathematics conference and saying that they actively use it in their classes

[Patrick Massot]

Did you try navigating https://impermeable.github.io/? Most links lead to blank pages.

[Eric Wieser]

It looks like they're all supposed to redirect to https://impermeable.github.io/src/default.html, which isn't much better

[Heather Macbeth]

Interesting, I never saw that paper before. I like their LaTeX-formatted proof environment!

It's nice to see that that paper includes an implementation of an Isabelle/Lean-style calc environment for Coq, I wonder if that will be incorporated into Coq standard libraries. I still think the Lean calc-syntax is nicer, though. Their calcs are one-liners and that would get unwieldy on nontrivial examples -- when I teach I encounter calcs like

  calc d (k + 2) = 3 * d (k + 1) + 5 * d k := by rw [d]
    _ ≥ 3 * 4 ^ (k + 1) + 5 * 4 ^ k := by rel [IH1, IH2]
    _ = 16 * 4 ^ k + 4 ^ k := by ring
    _ ≥ 16 * 4 ^ k := by extra
    _ = 4 ^ (k + 2) := by ring

all the time.

[Marcello Seri]

Patrick Massot said:

Did you try navigating https://impermeable.github.io/? Most links lead to blank pages.

No, I did not. I had only played with it on the laptop of the speaker