I had always thought you were just switching to a focus on formal methods! Otoh we had only interacted a teeny bit / little to none while you were in nyc I think
Probably worth noting that I did have an PhD offer earlier, to work with Coq. However, since it was in a small village in Germany, I had to turn it down.
On a more general note, I don't know if formal methods is that promising today: proof assistants are very immature, and proving even little things involves a lot of trial-and-error and is very time-consuming.
Yes, I recall interacting with you!