似乎北美搞类型论的人，长期留在学校里搞科研的也不算很多，一个时代大发展时期一些学者就占据了高高校和学派的有利位置，然后的学生没多少特别重要的突破性工作可以做了，也都去产业搞工业验证和编程去了。北欧可能稍微好点，但是考虑到每年PhD毕业的那么多量，继续搞学术的还是比例很低的。
AI说即使AI大发展，搞类型论的人也没有减少，各种学术会议文稿件数量仍然在稳步增长，可能也是因为Coq/Agda里容易出论文吧。
发布于 上海
概念机器