Much like that day a while ago that was "omg music all day" today has been kind of "omg math* all day". Advisor meeting was followed by a few hours of discussion of various LF/logic/type theory/focusing/etc. issues with Dan Licata and wjl. Went to D's after that, which resulted in more general talk of what a proof is, a short interlude about IF logic because austin was interested in it, and then dinitz trying to explain neat complexity theory results. * or otherwise formal thinking of some kind.