Thank you. 1. I'd heard of Agda but never read any code. What a brilliant language. I've added it to my list of my languages to spend time with. 2. I think yo

Thank you. 1. I'd heard of Agda but never read any code. What a brilliant language. I've added it to my list of my languages to spend time with. 2. I think your experience with Agda, especially the realisation that programs = proofs, leading to the Curry-Howard correspondence is exciting and rightfully bumps Agda to the top of my list. Functional programming has also opened my eyes with type systems too. That actually, an inconsistent and weak type system is a bigger liability than once thought - I'm realising that daily. Especially with null values and "trying to call method on non-object" errors.