Related to that last boost, I have no idea why my thesis title included the word "Practical". I don't think I've ever done anything less practical.

(It is kind of entertaining watching the history of the word "practical" in relation to dependently typed programming though. Are we nearly there yet?)