Fwiw I am wanting to give a lecture on dependent types in my class and while coq is the only prover I really know I am so hesitant to talk about its name that I’m considering learning agda 😂 😂
Conversation
Have you considered F* or Lean?
1
2
I didn’t consider F* for this application, but I might try Lean. I think for the purposes here, the concrete tool doesn’t matter too much and most of the base type theories are roughly similar at the level my students will see them
1
2
I like how Lean makes it easy to move between term-based proofs and tactic based proofs. One reason I like Idris and Agda early on was that things weren't obscured by tactics, but I've since learned the value of tactics for more involved stuff.
I'd imagine that tactics are eaiser for those coming from a mathematical background, but as a programmer it was eye-opening to be able to make proofs just using pattern matching, data constructors, recursion, etc. If that makes sense!
1
2
for sure, yeah, I'm working on a short writeup right now about self-certifying interpreters in racket that produce proofs--where the proofs are checked using a dynamic predicate, and then builds up to using coq to do this in both gallina (fixpoint) / tactics (theorem)
1