Thank you! My work laptop is a M4 Macbook Pro so I really appreciate the beauty of Rosetta. Thank you for the effort!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&#x2F;CS school IMO in my country - at the age of 40+ I&#x27;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: ( <a href="https:&#x2F;&#x2F;uwspace.uwaterloo.ca&#x2F;items&#x2F;4bc518ca-a846-43ce-92f0-806c18cc7811" rel="nofollow">https:&#x2F;&#x2F;uwspace.uwaterloo.ca&#x2F;items&#x2F;4bc518ca-a846-43ce-92f0-8...</a> ), but it doesn&#x27;t look like it&#x27;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&#x27;t take any serious Algebra classes and understand nothing of your paper)

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

Do you have book recommendations in regards to disassembly, syscalls, x86&#x2F;64 assembler etc?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&#x2F;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)?

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&#x2F;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&#x2F;authority and&#x2F;or the business case needs to be very evident.

We&#x27;re you really _the_ creator of Rosetta 2? How big was the team, what was your role in it?Rosetta 2 is amazing, I&#x27;m genuinely surprised this is the work of just one person!

You can use floats to accelerate interval arithmetic (which is &quot;exact&quot; 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 &quot;small&quot; (for unclear definitions of &quot;small&quot;, 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.

sorry to hijack the discussion but do you see any chance of consolidating the theoretical framework of real numbers with practical calculations of floats?
That is if I proof the correctness of some theorem for real numbers ideally I would just use that as the algorithm to compute things with floats.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?

This is exciting!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?

I don&#x27;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&#x27;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

What was the tipping point that made you want to work on Lean?

I don&#x27;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&#x27;t necessarily that interesting (i.e. intellectually stimulating) and it can be frustrating working in a field with this much noise.

Surprised you didnt go into something AI adjacent

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.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.<a href="https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=28914208">https:&#x2F;&#x2F;news.ycombinator.com&#x2F;item?id=28914208</a><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>

<a href="https:&#x2F;&#x2F;lean-fro.org&#x2F;about&#x2F;" rel="nofollow">https:&#x2F;&#x2F;lean-fro.org&#x2F;about&#x2F;</a>

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

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

<a href="https:&#x2F;&#x2F;lean-lang.org&#x2F;lean4&#x2F;doc&#x2F;" rel="nofollow">https:&#x2F;&#x2F;lean-lang.org&#x2F;lean4&#x2F;doc&#x2F;</a>

Background about the organization: <a href="https:&#x2F;&#x2F;en.m.wikipedia.org&#x2F;wiki&#x2F;Convergent_Research" rel="nofollow">https:&#x2F;&#x2F;en.m.wikipedia.org&#x2F;wiki&#x2F;Convergent_Research</a>Their proof assistant &#x2F; programming language: <a href="https:&#x2F;&#x2F;en.m.wikipedia.org&#x2F;wiki&#x2F;Lean_(proof_assistant)" rel="nofollow">https:&#x2F;&#x2F;en.m.wikipedia.org&#x2F;wiki&#x2F;Lean_(proof_assistant)</a>

&quot;we aim to tackle the challenges of scalability, usability, and proof (Mathematics) automation in the Lean proof assistant.&quot;

Its not weird its just disgusting. The back button should go back

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

The 20th million doesn&#x27;t hit as hard as the 19th and when you make 2x your salary on the dividends on your stock you start to wonder why not just do something more interesting.

Sometimes people just want to work on cool stuff and have the luxury of being able to do that. Rosetta 2 is shipped and done.

Citation needed?I mean, there will always be long tenured people leaving, even without offers on the tableSome jobs get old eventually

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.

<a href="https:&#x2F;&#x2F;youtu.be&#x2F;4Or-5OLCNDA?si=mzd_o0573HPgCVrl&amp;t=51" rel="nofollow">https:&#x2F;&#x2F;youtu.be&#x2F;4Or-5OLCNDA?si=mzd_o0573HPgCVrl&amp;t=51</a>

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

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