Rosetta 2 creator leaves Apple to work on Lean full-time (opens in new tab)

> May I ask, what is the path that leads you to the Rosetta 2 project?

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.

Waterloo really is the best CS school in the world.

Thanks. It means a lot coming from someone with experience in our niche field.

I was the only person working on it for ~2 years, and I wrote the majority of the code in the first version that shipped. That said, I’m definitely glad that I eventually found someone else (and later a whole team) to work on it with me, and it wouldn’t have been as successful without that.

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.

It is my experience that it is easier to create good quality things as an individual than as a team. Especially for the core of a product. Also look at Asahi.

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.

"Virtual Machines: Versatile Platforms for Systems and Processes" by Jim Smith and Ravi Nair is a great book on the topic.

I did go to Mozilla Research to work on Servo/Rust for a bit in 2015, which didn’t turn out to be the best decision.

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.

You can use floats to accelerate interval arithmetic (which is "exact" in the sense of constructive real numbers) but that requires setting the correct rounding modes, and being aware of quirks in existing hardware floating point implementations, some of which may e.g. introduce non-exact outputs in several of the least significant digits, or even flush "small" (for unclear definitions of "small", not always restricted to FP-denormal numbers) results to zero.

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.

I don't think there was a single tipping point, just a growing accumulation of factors:

- 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

I don't know what his reasons are but it makes sense to me. Yes, there are incredible results coming out of the AI world but the methods aren't necessarily that interesting (i.e. intellectually stimulating) and it can be frustrating working in a field with this much noise.

Lean is AI adjacent.

This is *VERY* AI-adjacent... the next batch of AI algos will need to integrate reasoning through theorem provers to go next level

All this stuff is or was proprietary, closed-source tech, and what's more, it was tech that gave certain companies strong competitive advantage at particular points in time -- so they had strong incentives to make sure it did not leak.

(I see posters in this thread who do not know what I thought were well-documented parts of the story, so I am trying to spell out the context here.)

Some large reputable companies have histories of stealing other's code, ideas, implementation methods, algorithms etc. and passing them off as their own. IBM, Microsoft, Sun, Apple, Google, Oracle, Digital Research, Lotus -- all were dominant players, all were so accused. Most either backed down, or re-wrote, or re-implemented to avoid being sued.

Microsoft more than almost anyone, and it only thrived because it was able to pay other companies off, or simply wait for them to go broke.

Sometimes, how code works can be deduced simply by studying what it does. I worked out how Rsync worked because someone asked me to explain what it did in detail.

Powerquest's PartitionMagic was amazing, black magic tech when it came out. I didn't review v1 because I did not believe what the packaging said; when I reviewed v2, a reader wrote in accusing my employers of doing an elaborate April Fool's joke and pointed out that my name is an anagram of APRIL VENOM.

(If I ever branch out into fiction, that's my pseudonym.)

Now, the revolutionary functionality of PartitionMagic is just an option in one screen of some installation programs. It's valueless now. Once people saw it working, they could work out how it was done, and then do it, and it ceased to have value.

Very fast emulation is not such a thing. Setting aside sheer Moore's Law/Dennard scaling brute horsepower, efficient emulation during the short window of processor architecture transitions is a massive commercial asset.

Apple has done it 3 times between 4 architectures.

68000 -> PowerPC PowerPC -> x86 x86-64 -> Arm64

Nobody else has ever done so many.

IBM bought Transitive for QuickTransit, but it's not clear how it used it. Its major architecture change was IBM i. Originally OS/400 on AS/400, a derivative of the System 36 minicomputer, it successfully moved this to POWER servers. However, there is a translation layer in the architecture, so it didn't need Transitive for that.

But IBM has bought many radical tech companies and not used the tech. E.g. Rembo, an amazing Linux-based boot-time network-boot fleet deployment tool it never really commercialised.

Microsoft bought Connectix for VirtualPC, kept the disk formats and management UI and threw away everything else, because Intel and AMD bundled the core virtualisation tech.

I know a little of the binary translation tech because the man who wrote it flew across the Altantic for me to interview him.

All thrown away, but today, it's valueless anyway.

At the time, though, very valuable.

Yeah that really doesn’t help.

There are a lot of broken links in the docs. Like most of the feature links.

That answers the Lean part, FRO stands for Focused Research Organization

The audio on this is about the worst I’ve ever heard on YouTube. I fast forwarded and at least he stops playing that loud music over his quiet voice, but damn.

He gets off topic a lot (bullies, amphetamine salts??) and spends the entire time talking to the commenters not the video recording.

Surely, there’s a better video out there than this.