Rosetta-2-Entwickler Cameron Zwarich verlässt Apple und wechselt zu Lean FRO

• Cameron Zwarich, der sich bei Apple mehr als 15 Jahre mit systemnaher Software auf niedriger Ebene beschäftigt hat, ist zu Lean FRO gewechselt
• Zwarich wird als Schöpfer von Rosetta 2 vorgestellt; damit wechselt Erfahrung aus der Systemsoftware in den Lean-Bereich
• Der Schwerpunkt bei Lean FRO liegt auf der Verbesserung des Codegenerators von Lean
• Leonardo de Moura begrüßt Zwarich als herausragenden Softwareentwickler und erwartet, dass seine Expertise das Lean-Ökosystem beeinflussen wird
• Dieser Wechsel kann als Teil der Entwicklung gesehen werden, in der Lean über Proof-Tools hinaus auch Ausführungsleistung und die Compiler-Schicht stärken will

---

Cameron Zwarich wechselt zu Lean FRO

• Cameron Zwarich ist zu Lean FRO gewechselt
• Leonardo de Moura begrüßt Zwarich als Schöpfer von Rosetta 2 und als herausragenden Softwareentwickler
• Zwarich verfügt über mehr als 15 Jahre Erfahrung mit systemnaher Software auf niedriger Ebene bei Apple

Rolle bei Lean

• Zwarichs Hauptaufgabe bei Lean FRO ist die Verbesserung des Codegenerators von Lean
• de Moura erwartet, dass seine Expertise großen Einfluss auf das Lean-Ökosystem haben wird
• Im Beitrag sind außerdem die Hashtags #LeanLang, #LeanProver, #LeanFRO enthalten

[GN⁺]

Meinungen auf Hacker News

• Das bin ich! Ich hätte nicht gedacht, dass das hier landet, aber ich freue mich darauf, gemeinsam mit Lean FRO und anderen aus der breiteren Lean-Community daran zu arbeiten, Lean besser zu machen.
  Mein Hintergrund ist Mathematik, und ich interessiere mich schon seit der Zeit vor meiner Laufbahn als professioneller Software Engineer für interaktive Theorembeweiser. Dass ich das nun in Vollzeit machen kann, kommt der Erfüllung eines Traums ziemlich nahe.
  • Mein Arbeitslaptop ist ein M4 MacBook Pro, daher weiß ich die Schönheit von Rosetta wirklich zu schätzen.
    Laut LinkedIn sind Sie seit 2009 bei Apple gewesen, abgesehen von einem Jahr bei Mozilla zwischendurch. Ich habe auch gesehen, dass Sie an der University of Waterloo in reiner Mathematik promoviert haben; persönlich halte ich Waterloo für die beste Mathematik-/Informatik-Hochschule unseres Landes, und selbst jetzt, in meinen Vierzigern, würde ich ohne Zögern hingehen, wenn sie mich nur aufnehmen würden.
    Mich würde interessieren, über welchen Weg Sie zum Rosetta-2-Projekt gekommen sind. Ich habe mir auch Ihre Dissertation angesehen, aber https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... schien keinen Bezug zur Compiler-Theorie zu haben.
    Ich habe früher ebenfalls Mathematik studiert, war aber kein guter Student; ich habe Statistik gemacht und scherzhaft gesagt, das sei kein Teil der Mathematik, daher habe ich keine ernsthaften Algebra-Kurse belegt und verstehe diese Arbeit überhaupt nicht.
  • Rosetta 2 ist eines der technisch beeindruckendsten Ergebnisse, die ich je gesehen habe. Obwohl ich selbst ziemlich tief mit DynamoRIO an Binärübersetzung gearbeitet habe, fühlt sich Rosetta 2 immer noch wie Magie an.
  • Sind Sie wirklich der Entwickler von Rosetta 2? Mich würde interessieren, wie groß das Team war und welche Rolle Sie hatten.
    Rosetta 2 ist erstaunlich; wenn das die Arbeit einer einzigen Person war, wäre ich wirklich verblüfft.
  • Gibt es Bücher, die Sie zu Disassemblierung, System Calls und x86/64-Assembler empfehlen würden?
    Mich interessiert, was man wissen muss, um etwas so Ausgefeiltes wie Rosetta zu bauen.
    Ich vermute, dass Sie die System Calls der jeweiligen Host-/Guest-Systeme als zuverlässige Abstraktionsschicht neu implementiert und getestet haben, aber es gibt so viele Aspekte, die weit über mein Verständnis hinausgehen.
    Haben Sie auch einen eigenen Assembler-Debugger gebaut? Mich würde interessieren, welche Tools Sie bei der Arbeit verwendet haben und ob Reverse-Engineering-Tools wie Ghidra oder Binary Ninja nützlich waren.
  • Wenn jemand seit 2009 mindestens bei FAANG war, frage ich mich, ob er schon einmal in Rente gegangen ist oder ein Sabbatical von ein bis zwei Jahren genommen hat.
    In der Zeit könnte man genug verdient haben, um im Ruhestand von passivem Einkommen in ungefährer Höhe eines Gehalts zu leben, und steuerlich wäre das vermutlich viel günstiger gewesen.
    Mich interessiert ganz unvoreingenommen, wie diese Entscheidung zustande kam. Wenn FAANG oder insbesondere Apple erfüllend war, ist das natürlich völlig in Ordnung; da ich auf Blind viele solche Fälle gesehen habe, frage ich mich aber auch, ob da eine fast irrationale finanzielle Unsicherheit eine Rolle spielt.
• In einer früheren Diskussion fiel der Name Gary Davidian; auch er hat bei Apples Architekturwechsel anfangs fast allein Erstaunliches geleistet. Im Archiv des Computer History Museum gibt es ein Interview.
  https://news.ycombinator.com/item?id=28914208
  https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
  • Dem Wiki zufolge scheint Davids Emulator Interpretation verwendet zu haben, während Erics dynamische Rekompilierung nutzt; die Connectix-Version war schneller, also dürften dort mehr Optimierungen eingeflossen sein.
    Ich habe versucht, den Quellcode zu finden, aber nichts gefunden.
• Der Zurück-Button von LinkedIn ist seltsam. Wenn man auf Zurück klickt, kommt man nicht zu HN zurück, sondern landet auf der LinkedIn-Startseite.
  • Das ist nicht seltsam, sondern widerlich. Zurück sollte zur vorherigen Seite zurückführen.
• Was ist Lean FRO?
  • https://lean-fro.org/about/
  • Lean ist derzeit eine Nischen-Programmiersprache und ein Proof Assistant.
    Ein Proof Assistant ist im Grunde ein Werkzeug zum Konstruieren mathematischer Beweise und überprüft, ob ein Beweis korrekt ist, so wie ein Compiler die Typen eines Programms überprüft.
    Soweit ich es verstehe, entsprechen, wie Curry und Howard entdeckt haben, auch allgemeine Programmiersprachen mit bestimmten Einschränkungen einem Proof Assistant. Mit Einschränkungen ist hier etwas in der Art gemeint, dass Rust im Vergleich zu Java erzwingt, bestimmte Regeln einzuhalten.
  • Hintergrund der Organisation: https://en.m.wikipedia.org/wiki/Convergent_Research
    Ihr Proof Assistant/ihre Programmiersprache: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
  • https://lean-lang.org/lean4/doc/
  • „Ziel ist es, die Herausforderungen rund um Skalierbarkeit, Benutzerfreundlichkeit und Beweisautomatisierung (Mathematik) im Lean-Proof-Assistant anzugehen.“
• Wie finanziert sich die gemeinnützige Lean-Organisation, sodass sie sich derart herausragende Entwickler leisten kann? Ich frage mich, wie solche Strukturen im Allgemeinen funktionieren.
• Es wirkt, als verliere Apple an verschiedenen Stellen Talente. Ich frage mich, was intern vor sich geht, dass Leute in einer Zeit wie jetzt, in der der Arbeitsmarkt unsicher ist, gehen.
  • Die zwanzigste Million Dollar fühlt sich nicht mehr so bedeutend an wie die neunzehnte, und wenn man mit Dividenden aus gehaltenen Aktien das Doppelte seines Gehalts verdient, fragt man sich irgendwann, warum man nicht einfach an etwas Interessanterem arbeiten sollte.
  • Manche Leute wollen einfach coole Arbeit machen und haben auch die Freiheit dazu. Rosetta 2 ist bereits veröffentlicht und ein abgeschlossenes Projekt.
  • Das hätte man auch 1985 sagen können, und es wäre richtig gewesen. Talentierte Leute haben Optionen.
  • Dafür bräuchte es Belege.
    Es kommt immer vor, dass langjährige Mitarbeiter gehen, und selbst wenn es kein angebotenes anderes Ziel gibt, fühlt sich eine Tätigkeit irgendwann einfach alt an.