I initially kept that option open, yes. However, there are surprisingly few available positions in formal methods outside of academia, and Coq is very very hard: my ability to prove things with Coq is quite modest.
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.
I would have gone with the small village in Germany! But yes, formal methods will likely be eclipsed by machine learning applications due to the investment in skills required and time consuming nature of the activities.
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!