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.
I just checked your LinkedIn and realized you joined Apple since 2009 (with one year of detour to Mozilla). You also graduated from Waterloo as a Pure Math Graduate student (I absolutely love Waterloo, the best Math/CS school IMO in my country - at the age of 40+ I'd go without doubt if they accept me).
May I ask, what is the path that leads you to the Rosetta 2 project? I even checked your graduate paper: ( https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... ), but it doesn't look like it's related to compiler theory.
(I myself studied Mathematics back in the day, but I was not a good student and I studied Statistics, which I joked that was NOT part of Mathematics, so I didn't take any serious Algebra classes and understand nothing of your paper)
The member of senior management who was best poised to suggest who should work on it already knew me and thought I would be the best choice. Getting opportunities in large companies is a combination of nurturing relationships and luck.
... not to mention all the performance considerations and optimizations, also requiring a strong sense of algorithms and computational complexity. Wow!
Yeah, seems like most mathematicians (and physicists) I know who go into tech don't get past learning a couple of programming languages and don't have an interest in learning the depths of a how a computer works. Very impressive!
I originally wasn’t going to go to university, but my parents suggested I go for CS. I transferred into Pure Math in my first term after the intro Java programming course asked us to implement tic-tac-toe without using arrays.
Basically all of the low-level programming and systems stuff was learned on the job, but it helped that my first job at Apple was working on WebKit’s interpreter (and later JIT), coming out of a Google Summer of Code doing the same thing. One of my coworkers on that project was an alumnus of the original Rosetta from Transitive, and he later ended up managing the group doing the transition to Apple silicon on the SWE side (I was part of HW Technologies). An interesting example of how things loop back in the industry.
This now makes sense you were able to work on Rosetta 2 mainly on your own!
Eventually figured out I'm more into comp arch, assembly language and such instead of the more Math part of CS.
I kinda agreed with him.
I don’t remember the actual requirement, unfortunately.
> Students admitted at the 1A level (except for those in Business Administration and Computer Science double degree), will normally have eight academic terms and six work terms.
Six work terms seem to be a LOT. Most coops I know is just a few summers.
Rosetta 2 is amazing, I'm genuinely surprised this is the work of just one person!
When people think of a binary translator, they usually just think of the ISA aspects, as opposed to the complicated interactions with the OS etc. that can consume just as much (or even more) engineering effort overall.
How do you communicate with the rest of the organization? What is the lifecycle and release process like? Do you write requirements and specs for others (like validation or integration) to base their work on? Basically, what does the day to day work look like?
As far as Rosetta in particular was concerned, I think I was just in the right environment to consistently be in a flow state. I have had fleeting moments of depression upon the realization that I will probably never be this productive for an extended period of time ever again.
On your last point, I’ve felt something like that myself and I hold onto hope that it isn’t true for myself (and now for you in your future endeavors). But even if it is true, you achieved something superhuman in your niche and the vast majority of people throughout the history of time have no idea what that is like. Tasting Heaven cannot last too long while on Earth. Maybe AI will bring us a little bit closer to that Heaven.
I wonder if Apple's renowned secrecy is a help with this. If nobody outside your small team knows what you are doing then it is hard for them to stick their oar in.
I'd imagine a lot of people are willing to do things for free.
QEMU was something like a factor of 5-10x slower than native, IIRC.
Flags are also tricky, though they're pretty well optimized. In the end the main issue with them is also the spilling, but QEMU's generic architecture makes it expensive to handle consecutive jump instructions for example.
It's a huge achievement for a single person to have written most of that.
Qemu was mostly Fabrice Bellard by himself at the beginning and plenty of emulators are single person project.
It’s a field which lends itself well to single person development. How to properly architecture compiler/interpreter/emulator has been studied to death and everyone mostly uses the same core principles so there is little guess work as how to start (provided you have taken the time to study the field). If you are ready to do the work, you can reach a working translator from hard work alone. Then, the interesting work of optimising it starts.
Don’t get me wrong, Rosetta 2 is a very impressive achievement because the performances are really good. I tip my metaphorical hat to whoever did it. My post is more in the spirit of you can do something in the same ballpark too if that’s your kick.
I don't understand why Apple even bothers these days, I wouldn't be surprised if Apple's gaming market is a quarter of what the Linux gaming market currently is (thanks to Valve and their work on proton and by extension wine)...
If Apple truly cared, they would stop blocking older games from being run on newer versions of OSX...
https://techcommunity.microsoft.com/blog/sqlserver/azure-sql...
There's probably other closed-source linux software being distributed as amd64-only binaries (rosetta 2 for linux VMs isn't limited to docker containers).
It made financial sense to stop paying the licensing fee to include it in each new version of the OS as quickly as possible.
There is no financial incentive to remove the current version of Rosetta, since it was developed in-house.
However, to really finish/polish a product you need a larger group of people. To get the UI just right, to get the documentation right, to advocate the product, to support it.
It is easily possible to have 10 people working on the team and only having a single core person. Then find someone to act as product manager while as the core person you can focus on the core of the product while still setting the direction without having to chase all the other work.
It is possible, but not easy to set up in most organisations. You need a lot of individual credit/authority and/or the business case needs to be very evident.
What do I need to know to be able to build something as advanced as rosetta?
I am assuming that you reimplemented the syscalls for each host/guest system as a reliable abstraction layer to test against. But so many things are way beyond my level of understanding.
Did you build your own assembler debugger? What kind of tools did you use along the way? Were reversing tools useful at all (like ghidra, binaryninja etc)?
Just curious how the decisions have formed, its totally fine if FAANG or specifically Apple was fulfilling for you, I also wonder if its financial fear to an irrational extent just because I see that on Blind a lot
I always assumed that I would stick around at Apple until some singular event that would motivate me to quit, and that would be it. I have been so lucky at Apple to have been in the right place at the right time for several projects: relatively early iPhone team, original iPad team, involved in the GCC -> Clang transition, involved in the 64-bit ARM transition, involved in early Apple Watch development, first engineer working full-time on the Apple silicon transition for the Mac, etc. Obviously I was doing something right if I kept getting these chances, but if I went to another FAANG I wouldn’t have the same history, and I don’t think it would be the same experience.
My projected path to parting ways with Apple didn’t really take place, since I’m now working at a non-profit dedicated to developing an interactive theorem prover and left Apple without any animosity in either direction.
Thanks for all that incredible work and your insights here.
also I was shocked to learn that the simple general comparison of (the equality of) two real numbers is not decidable, which is very logical if you think about it but an enormous hindrance for practical applications. Is there any work around for that?
Equality is not computable in the general case, but apartness can be stated exactly. For some practical cases, one may also be able to prove that two real numbers are indeed equal.
Given your experience with Rosetta 2 and your deep understanding of code translation and optimization, what specific areas in Lean’s code generation pipeline do you see as ‘low-hanging fruit’ for improvement?
Additionally, which unique features or capabilities of Lean do you find most promising or exciting to leverage in pushing the boundaries of efficient and high-quality code generation?
- the release of Lean 4 slightly over a year ago, which impressed me both as a proof assistant and a programming language
- the rapid progress in formalization of mathematics from 2017 onward, almost all of which was happening in Lean
- the growing relevance of formal reasoning in the wake of improvements in AI
- seeing Lean's potential (a lot of which is not yet realized) for SW verification (especially of SW itself written in Lean)
- the establishment of the Lean FRO at the right time, intersecting all of the above
Fellow physicist here by the way
You're right that "but humans also" is better than my "and humans also"
But then I think about how maddeningly unpredictable human thought and perception is, with phenomena like optical illusions, cognitive biases, a limited working memory. Yet it is still produces incredibly powerful results.
Not saying ML is anywhere near humans yet, despite all the recent advances, but perhaps a fully explainable AI system, with precise logic, 100% predictable, isn’t actually needed to get most of what we need out of AI. And given the “analog” nature of the universe maybe it’s not even possible to have something perfect.
I agree with your general point (I think), but I think that "unpredictable" is really the wrong word here. Optical illusions, cognitive biases and limited working memory are mostly extremely predictable, and make perfect sense if you look at the role that evolution played in developing the human mind. E.g. many optical illusions are due to the fact that the brain needs to recreate a 3-D model from a 2-D image, and it has to do this by doing what is statistically most likely in the world we live in (or, really, the world of African savannahs where humans first evolved and walked upright). This, it's possible to "tricks" this system by creating a 2D image from a 3D set of objects that is statistically unlikely in the natural world.
FWIW Stephen Pinker's book "How the Mind Works" has a lot of good examples of optical illusions and cognitive biases and the theorized evolutionary bases for these things.
It helps that work done in Lean (on Mathlib and other developments) is reaching an inflection point just as these questions become practically relevant from AI.
Of course it has many non-AI uses too.