For dependently-typed programming, I've been tinkering with [Idris](https://www.idris-lang.org/) recently as it's the friendliest language, was thinking of writing a parser for to turn [Quantities](https://github.com/timjb/quantities) into something like [Qalculate](http://qalculate.github.io/). I intend to look more into [ATS](http://www.ats-lang.org/) as it's seemingly feature-packed. In the past, I've used Coq for the Software Foundations class, and also given Agda a spin.

As for economics, I've been looking into the work of Von Neumann, Nash, Arrow and Debreau, and their methodology of using fixed-point theorems (Lawvere shows how they are non-constructive in *Conceptual Mathematics*), as well as the resultant divides it created (such as the spat between Solow and Robinson within Keynesian economics). I've done a little looking into the broader history of how money has been used over time (*Debt: The First 5000 years* has much on this), how Fibonacci introduced double-entry bookkeeping and Hindu-Arabic decimal notation to the Florentines, enabling the Medicis to create the first international banks, through to Keynes and the failures of the Bretton-Woods system in the 20th century (both *The General Theory of Interest, Employment, and Money* and *Modern Political Economics*). Also have started looking into David Ellerman's work now, such as his work on property theory at the suggestion of Keith.