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

Original Article ↗ Hacker News Discussion ↗

A key engineer behind Apple’s Rosetta 2 binary translation system has left the company to work full‑time on Lean, a formal proof assistant that doubles as a programming language. Commenters explore what Lean and the new Lean Focused Research Organization aim to achieve—scalable, usable, partially AI‑assisted formal verification of mathematics and software—and why this is increasingly relevant as AI systems generate more complex proofs. The thread also highlights how one person initially built most of Rosetta 2, the dynamics of doing deep systems work inside large companies, and the broader trend of well‑compensated engineers leaving Big Tech to pursue intellectually driven projects.

What Lean FRO and Lean Are

  • Lean FRO is described as a “Focused Research Organization” working on the Lean proof assistant / programming language, targeting scalability, usability, and proof automation.
  • Several commenters find the official explanation and site UX confusing or too abstract, especially for those without a proof-assistant background.
  • Links to Lean 4 docs and a new language reference are shared; some documentation links are currently broken.
  • Background links describe Lean as a proof assistant / programming language and Lean FRO as part of a broader “convergent research” model.

Lean, Proof Assistants, and AI

  • Lean is characterized as a niche programming language and proof assistant, rooted in type theory and related to the Curry–Howard correspondence.
  • Multiple commenters emphasize that while Lean is not machine learning, it is highly “AI-adjacent”:
    • It offers a formal verification layer for AI-generated proofs at scale.
    • It’s seen as critical for dealing with an emerging “epistemological crisis” in mathematics if AI generates many more proofs than humans can manually check.
    • Proof automation and symbolic reasoning are framed as part of “classical” AI (GOFAI), not just ML.
  • Lean FRO’s roadmap includes supporting AI organizations with tooling and data around math and science formalization.

Motivations and Career Path

  • The move from a major tech company to Lean FRO is explained as a cumulative decision:
    • Lean 4’s quality as language and proof assistant.
    • Rapid progress in formalized mathematics (especially in Lean).
    • Rising importance of formal reasoning due to AI.
    • Potential for software verification, especially self-hosted Lean code.
    • The timely creation of Lean FRO.

Rosetta 2 Technical Discussion

  • Rosetta 2’s quality and performance are widely praised; several note how close its performance is to native, compared to generic translators like QEMU.
  • It’s revealed that the initial Rosetta 2 implementation was largely developed by a single engineer for about two years, with a team added later.
  • Discussion highlights:
    • Specialized x86→ARM design vs. generic emulators.
    • Complexity from OS interactions, not just ISA translation.
    • Dynamic recompilation and flag handling as key performance themes.
  • Some debate whether Apple might eventually deprecate Rosetta 2:
    • One side points to the Rosetta 1 precedent.
    • Others argue this time is different due to extensive use in Linux VMs and Docker, and the absence of third-party licensing constraints.

Work Practices and Individual Productivity

  • Several comments explore how a single engineer can deliver a system like Rosetta:
    • Starting with a very small team avoids early coordination overhead and yields a tightly integrated core.
    • Later, the challenge becomes evolving a historically coherent core as new people join.
  • The author describes being in an unusually strong “flow state” for an extended period and doubts achieving that sustained productivity again.

Math, Reals, and Floats

  • One subthread asks about reconciling formal real-number proofs with practical floating-point computation and the undecidability of real equality.
  • Responses mention:
    • Using floats to accelerate interval arithmetic that is exact in a constructive sense.
    • Hardware quirks (rounding modes, denormals, flushing to zero) complicating exactness.
    • Equality of reals being non-computable in general, but “apartness” (proving inequality) often being expressible, and equality provable in special cases.

Apple Talent and Career Choices

  • Some view the departure as part of a broader “talent drain” at Apple; others push back, noting turnover is normal and high-earning employees may simply seek more intrinsically interesting work.
  • Financial security is seen as enabling moves to nonprofits or more intellectually satisfying but less lucrative work.

Unclear / Open Questions

  • How Lean FRO is funded and how it can hire top-tier developers is asked but not answered in the thread.