Maybe that would be better. I admit that I don't know the first thing about TLA+. Agda is what I learned about in school, and what my computer science friends a

Maybe that would be better. I admit that I don't know the first thing about TLA+. Agda is what I learned about in school, and what my computer science friends are excited about, and I was already interested in using it to write verified compilers. Writing compilers with functional languages was also a part of my university education. But that's just my background.