Rosetta 2 creator leaves Apple to work on Lean full-time

This is me! Didn’t expect to see this on here, but I’m looking forward to working with everyone else at the Lean FRO and the wider Lean community to help make Lean even better.<p>My background is in mathematics and I’ve had an interest in interactive theorem provers since before I was ever a professional software engineer, so it’s a bit of a dream come true to be able to pursue this full-time.

In a previous discussion the name of Gary Davidian is mentioned who also — initialy single-handed — did amazing work on architecture changes at Apple. There’s an interview with him in the Computer History Museum archive.<p><a href="https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=28914208">https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=28914208</a><p><a href="https:&#x2F;&#x2F;youtu.be&#x2F;MVEKt_H3FsI?si=BbRRV51ql1V6DD4r" rel="nofollow">https:&#x2F;&#x2F;youtu.be&#x2F;MVEKt_H3FsI?si=BbRRV51ql1V6DD4r</a>

The linkedin back button is weird. Instead of coming back to hn after back button, it goes to its homepage.

What is Lean FRO?

How is the Lean non-profit getting funded to be able to afford such great devs? How does that work in general?

I am pretty sure “lean” is that codeine cough syrup rappers drink

Apple just seems to be bleeding talent left and right. I wonder what&#x27;s going on over there to cause people to leave when the job market is as uncertain as it is right now.