Coq 8.13 - Hackdot

Re:Coq 8.13 by raptortech on Thursday February 18, 2021 @11:59AM (#26182310)

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

[ Parent | on HN ]

Re:Coq 8.13 by tracyhenry on Thursday February 18, 2021 @12:55PM (#26183145)

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.

[ Parent | on HN ]

Re:Coq 8.13 by mncharity on Thursday February 18, 2021 @02:04PM (#26184049)

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

[ Parent | on HN ]

Re:Coq 8.13 by mcncm on Thursday February 18, 2021 @12:16PM (#26182557)

Any chance you took FRAP last spring? Hi, maybe-classmate :)

[ Parent | on HN ]

Re:Coq 8.13 by raptortech on Thursday February 18, 2021 @10:42PM (#26189396)

I'm taking it this semester!

[ Parent | on HN ]

Re:Coq 8.13 by mcncm on Tuesday February 23, 2021 @03:55PM (#26242755)

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!

[ Parent | on HN ]