The discussion in the post about dependent types is interesting, e.g.:
[…] I’m curious, who has promoted the myth that you need dependent types to do semantics
My experience is that teaching materials for Coq are much more developed in the context of semantics and software verification, despite Coq being harder to use.
The post mentions Concrete Semantics [1], which is a really nice Isabelle book. There’s also a Lean version [2]. However, to my best knowledge, there’s no intermediate/advanced teaching material such as [3-5] for Isabelle, Lean, or Agda. Just introductory stuff.
Sure, but what you said doesn’t relate to dependent types, it relates to the development of a tool and its surrounding community. That community also tends to believe that the absence of dependent types (and constructivism) makes a formal system not useful, which is what the comment in the post is about.
The discussion in the post about dependent types is interesting, e.g.:
My experience is that teaching materials for Coq are much more developed in the context of semantics and software verification, despite Coq being harder to use.
The post mentions Concrete Semantics [1], which is a really nice Isabelle book. There’s also a Lean version [2]. However, to my best knowledge, there’s no intermediate/advanced teaching material such as [3-5] for Isabelle, Lean, or Agda. Just introductory stuff.
[1] http://www.concrete-semantics.org
[2] https://raw.githubusercontent.com/blanchette/logical_verific…
[3] http://adam.chlipala.net/frap
[4] http://adam.chlipala.net/cpdt
[5] https://ilyasergey.net/pnp
Sure, but what you said doesn’t relate to dependent types, it relates to the development of a tool and its surrounding community. That community also tends to believe that the absence of dependent types (and constructivism) makes a formal system not useful, which is what the comment in the post is about.