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.
1
2
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!
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