Moonside OP wrote on January 14, 2018 at 7:42 PM

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

I'm doing it in Python and following ~TDD~

Reimplement in Coq and automatically derive it from specification. Actually I've tried to learn proper testing habits in Haskell, but I think that I don't even have a specification atm so yeah haha.

Godot looks pretty good.

I've been meaning to look at the Postmill source code and learn about that too

Me too! I've been itching to Fix a thing or two there.

twovests wrote on January 14, 2018 at 8:30 PM (edited on January 14, 2018 at 8:31 PM)

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

Moonside OP wrote on January 14, 2018 at 9:43 PM

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.