Le développeur de Rosetta 2, Cameron Zwarich, quitte Apple pour rejoindre Lean FRO

• Cameron Zwarich, qui travaille depuis plus de 15 ans sur les logiciels système bas niveau chez Apple, rejoint Lean FRO
• Zwarich est présenté comme le créateur de Rosetta 2, un exemple de transfert d'une expérience en logiciels système vers l'univers de Lean
• Chez Lean FRO, l'accent sera mis sur l'amélioration du générateur de code de Lean
• Leonardo de Moura accueille Zwarich comme un développeur logiciel exceptionnel et estime que son expertise aura un impact sur l'écosystème Lean
• Cette arrivée peut être vue comme un signe que Lean cherche à se renforcer non seulement comme outil de preuve, mais aussi en matière de performances d'exécution et de couche compilateur

---

Cameron Zwarich rejoint Lean FRO

• Cameron Zwarich rejoint Lean FRO
• Leonardo de Moura accueille Zwarich comme le créateur de Rosetta 2 et un développeur logiciel exceptionnel
• Zwarich possède plus de 15 ans d'expérience chez Apple, où il s'est spécialisé dans les logiciels système bas niveau

Rôle chez Lean

• Chez Lean FRO, la mission principale de Zwarich sera d'améliorer le générateur de code de Lean
• de Moura estime que son expertise aura un impact majeur sur l'écosystème Lean
• La publication inclut également les hashtags #LeanLang, #LeanProver, #LeanFRO

[GN⁺]

Avis sur Hacker News

• C’est moi ! Je ne pensais pas que ça arriverait ici, mais je suis ravi de travailler avec Lean FRO et d’autres personnes de la communauté Lean au sens large pour améliorer Lean.
  J’ai une formation en mathématiques, et je m’intéressais aux assistants de preuve interactifs avant même de devenir ingénieur logiciel professionnel, donc pouvoir faire ce travail à plein temps ressemble presque à un rêve devenu réalité.
  • Mon ordinateur portable de travail est un MacBook Pro M4, donc j’apprécie vraiment la beauté de Rosetta.
    En regardant LinkedIn, j’ai vu qu’il était chez Apple depuis 2009 et qu’à part une année passée chez Mozilla entre-temps, il était resté chez Apple. J’ai aussi vu qu’il venait d’un master/doctorat en mathématiques pures à Waterloo, et personnellement je considère Waterloo comme la meilleure école de mathématiques/informatique de notre pays ; même à la quarantaine, s’ils m’acceptaient, j’y irais sans hésiter.
    Je suis curieux de savoir par quel chemin il a rejoint le projet Rosetta 2. J’ai aussi consulté son mémoire de recherche de cycle supérieur, mais https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... cela ne semblait pas lié à la théorie des compilateurs.
    Moi aussi, j’ai étudié les maths autrefois, mais je n’étais pas un bon étudiant ; j’ai fait des statistiques, dont je dis parfois en plaisantant que ça ne fait pas partie des maths, donc je n’ai pas suivi de cours sérieux d’algèbre et je ne comprends absolument pas ce mémoire.
  • Rosetta 2 est l’un des résultats techniquement les plus impressionnants que j’aie vus de ma vie. J’ai travaillé assez en profondeur sur la traduction binaire avec DynamoRIO, et pourtant Rosetta 2 me paraît toujours magique.
  • Êtes-vous vraiment le créateur de Rosetta 2 ? Je suis curieux de connaître la taille de l’équipe et votre rôle.
    Rosetta 2 est stupéfiant ; si c’était réellement le travail d’une seule personne, ce serait franchement incroyable.
  • Auriez-vous des livres à recommander sur le désassemblage, les appels système et l’assembleur x86/64 ?
    Je me demande ce qu’il faut savoir pour construire quelque chose d’aussi sophistiqué que Rosetta.
    J’imagine que vous avez dû réimplémenter et tester les appels système de chaque système hôte/invité derrière une couche d’abstraction fiable, mais il y a tellement d’aspects qui dépassent largement mon niveau de compréhension.
    Avez-vous aussi créé votre propre débogueur assembleur ? Je suis curieux de savoir quels outils vous avez utilisés pendant le travail, et si des outils de rétro-ingénierie comme Ghidra ou Binary Ninja ont été utiles.
  • S’il est dans une FAANG depuis au moins 2009, je me demande s’il a déjà pris sa retraite ou pris une année sabbatique d’un an ou deux.
    À ce stade, il est possible qu’il ait gagné assez pour vivre à la retraite avec un revenu passif proche d’un salaire, avec une fiscalité bien plus avantageuse.
    Je suis simplement curieux de la manière dont cette décision s’est formée. Si FAANG, et Apple en particulier, lui convenaient, tant mieux évidemment ; mais comme j’ai vu beaucoup de cas de ce genre sur Blind, je me demande aussi s’il existe une anxiété financière presque irrationnelle.
• Dans une ancienne discussion, le nom de Gary Davidian avait été mentionné ; lui aussi avait fait au départ un travail impressionnant, presque seul, lors d’une transition d’architecture d’Apple. Il y a une interview dans les archives du Computer History Museum.
  https://news.ycombinator.com/item?id=28914208
  https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
  • D’après le wiki, l’émulateur de David semble utiliser de l’interprétation, tandis que celui d’Eric utiliserait de la recompilation dynamique ; la version de Connectix étant plus rapide, elle semble avoir davantage d’optimisations.
    J’ai essayé de trouver le code source, mais je n’ai rien trouvé.
• Le bouton retour de LinkedIn est bizarre. Quand on appuie sur retour, on ne revient pas sur HN, on arrive sur la page d’accueil de LinkedIn.
  • Ce n’est pas bizarre, c’est un comportement répugnant. Le retour doit ramener à la page précédente.
• Qu’est-ce que Lean FRO ?
  • https://lean-fro.org/about/
  • Lean est, pour l’instant, un langage de programmation et un assistant de preuve de niche.
    Un assistant de preuve est essentiellement un outil pour construire des preuves mathématiques, et il vérifie qu’une preuve est correcte de la même manière qu’un compilateur vérifie les types d’un programme.
    Si j’ai bien compris, comme l’ont découvert Curry et Howard, certains langages de programmation généraux soumis à des contraintes correspondent aussi à des assistants de preuve. Par contraintes, c’est un peu comme la façon dont Rust force à respecter certaines règles par rapport à Java.
  • Contexte de l’organisation : https://en.m.wikipedia.org/wiki/Convergent_Research
    Leur assistant de preuve/langage de programmation : https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
  • https://lean-lang.org/lean4/doc/
  • « Vise à traiter les défis de scalabilité, d’utilisabilité et d’automatisation des preuves (mathématiques) dans l’assistant de preuve Lean »
• Comment l’organisation à but non lucratif Lean se finance-t-elle pour pouvoir se permettre des développeurs aussi brillants ? Je suis curieux de savoir comment ce genre de structure fonctionne en général.
• Apple semble subir des départs de talents un peu partout. En cette période où le marché de l’emploi est incertain, je me demande ce qui se passe en interne pour pousser les gens à partir.
  • Le 20e million de dollars ne frappe pas autant que le 19e, et quand les dividendes de ses actions rapportent deux fois son salaire, on commence à se demander pourquoi ne pas simplement faire quelque chose de plus intéressant.
  • Certaines personnes veulent simplement faire des choses cool, et elles ont les moyens de le faire. Rosetta 2 est déjà sorti et le projet est terminé.
  • Cela aurait été vrai même si on l’avait dit en 1985. Les personnes talentueuses ont le choix.
  • Il faudrait des preuves.
    Il y a toujours des gens qui partent après être restés longtemps, et même sans offre ailleurs, certaines activités finissent par paraître dépassées.