You Got Your Idris in My C++! A First Look at Denotational Design
Programmers gripe that we have two kinds of programming languages: the ones we write in for fun, and the ones we write in because we have to. We may enjoy coding that weekend project in Agda, but we have to leave that smile behind on Monday morning when we go back to Java or C++.