>>20
I am not well versed in these things but Coq is based on something called the Calculus of Inductive Constructions, so probably yes. There are attempts to use it to teach proof heavy things, you can find papers about how successful these courses are, like these:
https://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf
https://dl.acm.org/doi/10.1145/3105726.3106184
https://cs.pomona.edu/~michael/papers/coqpl2019.pdf