Even my proof assistant / project pterodactyl. If someone beats me to building a satisfactory thing that meets my goals, that is fantastic because I can then move onto my actual goals: using it to learn and develop tons of mathematics that I am interested in.
Not one of my research projects is make-or-break. They are all designed to enable me to ^do^ something else that I want to do.
It’s similar to how, paraphrased, @david_chisnall is building CHERI so that he can one day get back to Étoilé OS (or a successor). We have to have a reason for doing what we are doing that is more than just collecting tokens.
Sep 29, 2026, 10:13 AM@jonmsterling It seems that a lot of type-theory research is done so that we can have our dream proof assistant to express Mathematics more beautifully. That we are able to do beautiful Mathematics along the way is just pure cherry-on-top (or in the case of @david_chisnall's research programme CHERI-on-top).
@jonmsterling basically yak-shaving turned into a professional practice