I'm from MIT EECS too. Just to clarify for other people - we have a pool of "required courses", from which we only need to choose a few. So it's not like we must learn Coq.
OTOH, I've TAed an undergrad research class and it's mind boggling how many people are doing Coq-related research.
The 6.822 page[1] has a draft[2] of Adam Chlipala's "Formal Reasoning About Programs", "introducing both machine-checked proof with [Coq] and approaches to formal reasoning about program correctness".
Aha, good luck then! I really enjoyed that class, even after things got derailed by Covid. It was like a little problem-solving adventure every week. Still wish there were more Coq in the real world!
Can you say more? My background is in PLT and my half-finished thesis was in Coq - but I've got a real interest in (human) languages too. I'd love to hear about how the two are intermingling.
Comments
What is the industry or academic prevalence or level of optimism for Coq / Lean?
Sample size of 1: I'm an EECS PhD student at MIT and one of my required courses (6.822) is taught entirely in Coq
I'm from MIT EECS too. Just to clarify for other people - we have a pool of "required courses", from which we only need to choose a few. So it's not like we must learn Coq.
OTOH, I've TAed an undergrad research class and it's mind boggling how many people are doing Coq-related research.
The 6.822 page[1] has a draft[2] of Adam Chlipala's "Formal Reasoning About Programs", "introducing both machine-checked proof with [Coq] and approaches to formal reasoning about program correctness".
[1] https://frap.csail.mit.edu/main [2] http://adam.chlipala.net/frap/frap_book.pdf
Any chance you took FRAP last spring? Hi, maybe-classmate :)
I'm taking it this semester!
Aha, good luck then! I really enjoyed that class, even after things got derailed by Covid. It was like a little problem-solving adventure every week. Still wish there were more Coq in the real world!
Theorem provers are increasingly popular in certain areas of linguistics.
Can you say more? My background is in PLT and my half-finished thesis was in Coq - but I've got a real interest in (human) languages too. I'd love to hear about how the two are intermingling.