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

Original Article ↗ Hacker News Discussion ↗

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.