C++, C, C#, Java
SML, Caml, Scheme, "fuzz" (the last being the little functional language that we made)
The remarkable thing is how unremarkable this is, I think; we all have to use various tools to get our work done.
Agda I've only been playing with in the evenings since ICFP, working on this little representational experiment with Dan Licata. Already I'm feeling very strongly that, e.g., Adam Chlipala's frequent advocacy of more automation in proof assistants is a valid point. Even if it's foolhardy to hope for sophisticated automated program synthesis (and even then it's probably not --- we are making pretty good progress there) there are so many little gaps that are essentially about constraint solving problems that are more often uniquely solvable than not. Twelf knows how to split cases on a type, but twelf-emacs-mode doesn't know how to textually insert a bunch of boilerplate and sheds for me --- but agda-emacs-mode does, and it makes me awfully happy.
This sort of benign, simple automation (well, to the extent that doing a bunch of higher-order unification in the background is simple...) really is playing the same role that type-checking per se is playing in the wider world of programming. One might say that the more macho hardcore programmer should be able to slice and dice all the invariants in their head without being a wimp and letting the compiler help them. But fuck that; me plus type inference is a more efficient system than me alone. Just like me plus a pocket calculator is a more efficient system than me alone, even though I might not be a mental-arithmetic whiz as a consequence. I can focus on the interesting difficulties and ignore the mechanically-solvable difficulties.