Hometown: Chiang Mai, Thailand
April 14, 2012
My favorite programming language depends on the application. For the kind of work I do now, ML is the best choice. I used to be interested in lazy languages like Haskell, but now think their runtime behavior is too hard to predict. I also used to be passionate about languages with dependent types, such as Agda and Epigram, but I have become a grumpy old man who no longer believes that Curry Howard is so compelling. I also gave up on ever understanding equality in those languages. I follow the development of programming languages and tools for meta programming (macros) with great interest. On a more practical note I would love to learn GWT with HTML5, but I have not yet found a compelling enough application to warrant the investment.
My main interest is in proof assistants. Since 2011 I work as independent researcher proving HOL Light correct in itself. Before that I worked as programmer in Henk Barendregts group in Nijmegen mainly on Coq.