We start with my addiction to programming books, and end with dependent types, that's a logical path, right?