Hormander

I'm spending the next 10 days in a frenzied attempt to
finish the Hormander real quantifier elimination algorithm
in HOL-Light. John is coming out with another release next
week and I want this to be in there. I spent all day, minus
a beautiful walk in Frick Park, working on it. I'm thinking
another 8 12-hour days and I'll be close. This project is
so typical of my innate procrastination. I was always
afraid to start/continue it because it takes me so long to
understand what is going on. If I just sit down and do the
darn work it goes smoothly. Well, at least there's visible
progress. More discipline needed...

I went to the Frick automobile museum during my walk
through the park. It was awesome! The first room has these
amazing old horse-drawn carriages. The second is full of
old Rolls-Royces and other early fancy cars. I won't forget
my camera next time I go.

"Paradoxically, then, William's great gift--for
confabulation-- which has been called out to leap
continually over the ever-opening abyss of amnesia--
William's great gift is also his damnation. If only he
could be \textit{quiet}, one feels, for an instant; if only
he could stop the ceaseless chatter and jabber; if only he
could relinquish the deceiving surface of illusions--then
(ah, then!) reality might seep in; something genuine,
something deep, something true, something felt, could enter
his soul."

--- Oliver Sacks, The Man Who Mistook His Wife for a Hat

A lucky shot out the UHaul window when I was moving to Astoria.