4 ms·
What is the industry or academic prevalence or level of optimism for Coq / Lean?
by threatofrain 6y ago
What is the industry or academic prevalence or level of optimism for Coq / Lean?
- raptortech 6y agoSample size of 1: I'm an EECS PhD student at MIT and one of my required courses (6.822) is taught entirely in Coq
- mcncm 6y agoAny chance you took FRAP last spring? Hi, maybe-classmate :)
- raptortech 6y agoI'm taking it this semester!
- mcncm 6y agoAha, 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!
- tracyhenry 6y agoI'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.
- mncharity 6y agoThe 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 https://frap.csail.mit.edu/main [2] http://adam.chlipala.net/frap/frap_book.pdf http://adam.chlipala.net/frap/frap_book.pdf
- sinkasapa 6y agoTheorem provers are increasingly popular in certain areas of linguistics.
- wk_end 6y agoCan 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.