Viewing a single comment thread. View all comments

twovests wrote (edited )

Reply to comment by Moonside in So what project are you working on? by Moonside

Ooh I never heard of Coq, I'll definitely need to check that out eventually! Googled it a bit, it seems neat but it'll be too much for me to get into rn

3

Moonside OP wrote

I was mostly joking, but I'm halfway done with the 1st of these books. It's definitely laborious, but interesting. It seems like things are faraway from production and changing pretty fast in that space. Some others: Agda, Idris, ATS (this seems scary). The most impressive Coq project I've seen is this C compiler: http://compcert.inria.fr .

Btw, juggling with proofs is very video game like though, I played with them too late into the night. That constant feedback! The triumph of writing Qed.

2