Cameron Zwarich, desarrollador de Rosetta 2, deja Apple y se une a Lean FRO

• Cameron Zwarich, quien ha trabajado durante más de 15 años en software de sistemas de bajo nivel en Apple, se une a Lean FRO
• Zwarich es presentado como el creador de Rosetta 2, en un caso donde su experiencia en software de sistemas se traslada al entorno de Lean
• Su enfoque en Lean FRO estará en mejorar el generador de código de Lean
• Leonardo de Moura le da la bienvenida a Zwarich como un destacado desarrollador de software y espera que su experiencia tenga impacto en el ecosistema de Lean
• Esta incorporación puede verse como parte de la tendencia de Lean de fortalecerse más allá de las herramientas de prueba, hacia el rendimiento de ejecución y la capa de compiladores

---

Cameron Zwarich se une a Lean FRO

• Cameron Zwarich se une a Lean FRO
• Leonardo de Moura le da la bienvenida a Zwarich como el creador de Rosetta 2 y un destacado desarrollador de software
• Zwarich tiene una trayectoria de más de 15 años especializado en software de sistemas de bajo nivel en Apple

Rol que asumirá en Lean

• La principal labor de Zwarich en Lean FRO será mejorar el generador de código de Lean
• de Moura espera que su experiencia tenga un gran impacto en el ecosistema de Lean
• La publicación también incluye los hashtags #LeanLang, #LeanProver, #LeanFRO

[GN⁺]

Comentarios de Hacker News

• ¡Soy yo! No esperaba ver esto aquí, pero me entusiasma trabajar junto con Lean FRO y otras personas de la comunidad más amplia de Lean para hacer que Lean sea mejor.
  Mi formación es en matemáticas, y como me interesaban los asistentes interactivos de demostración incluso antes de convertirme en ingeniero de software profesional, poder dedicarme a esto de tiempo completo es casi como un sueño hecho realidad.
  • Mi laptop de trabajo es una M4 MacBook Pro, así que realmente agradezco la belleza de Rosetta.
    Viendo LinkedIn, parece que estuvo en Apple desde 2009 y, salvo por un año en Mozilla en medio, siguió todo el tiempo en Apple. También vi que hizo posgrado en matemáticas puras en Waterloo, y personalmente creo que Waterloo es la mejor escuela de matemáticas/ciencias de la computación de nuestro país, así que aun ahora que estoy en mis 40, si me aceptaran iría sin dudarlo.
    Tengo curiosidad por saber por qué camino terminó participando en el proyecto Rosetta 2. También revisé su tesis de posgrado, https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8..., pero no parecía estar relacionada con teoría de compiladores.
    Yo también estudié matemáticas hace tiempo, pero no era buen estudiante; hice estadística, que en broma dicen que no forma parte de las matemáticas, así que no tomé cursos serios de álgebra y no entendí en absoluto esa tesis.
  • Rosetta 2 es de las cosas técnicamente más impresionantes que he visto en mi vida. Incluso habiendo trabajado bastante a fondo en traducción binaria con DynamoRIO, Rosetta 2 todavía se siente como magia.
  • ¿De verdad eres el creador de Rosetta 2? Me da curiosidad saber qué tan grande era el equipo y cuál fue exactamente tu rol.
    Rosetta 2 es increíble, y si esto fue obra de una sola persona, sinceramente me sorprendería muchísimo.
  • ¿Hay algún libro que recomiendes sobre desensamblado, llamadas al sistema y ensamblador x86/64?
    Tengo curiosidad por saber qué hay que aprender para construir algo tan sofisticado como Rosetta.
    Supongo que habrán reimplementado y probado las llamadas al sistema de cada sistema host/guest como una capa de abstracción confiable, pero hay demasiadas partes que están muy por encima de mi nivel de comprensión.
    ¿También hicieron su propio depurador de ensamblador? Me da curiosidad qué herramientas usaron durante el trabajo y si herramientas de ingeniería inversa como Ghidra o Binary Ninja fueron útiles.
  • Si estuviste al menos en FAANG desde 2009, me da curiosidad si alguna vez pensaste en retirarte o tomarte uno o dos años sabáticos.
    A esas alturas, probablemente ya habías ganado lo suficiente como para vivir retirado con un ingreso pasivo cercano a tu salario, y además la situación fiscal seguramente habría sido mucho más favorable.
    Tengo curiosidad genuina por cómo se formó esa decisión. Si FAANG, o Apple en particular, te satisfacía, entonces perfecto, pero como veo mucho ese tipo de casos en Blind, me pregunto si también hay una inseguridad financiera irracional.
• En una discusión anterior salió el nombre de Gary Davidian, y él también hizo al principio, casi en solitario, un trabajo asombroso en una transición de arquitectura de Apple. Hay una entrevista en el archivo del Computer History Museum.
  https://news.ycombinator.com/item?id=28914208
  https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
  • Según Wikipedia, parece que el emulador de David usaba interpretación, mientras que el de Eric usaba recompilación dinámica, y el de Connectix parece más rápido, así que da la impresión de que tenía más optimizaciones.
    Intenté encontrar el código fuente, pero no encontré nada.
• El botón de retroceso de LinkedIn se comporta raro. Aunque le des atrás, no vuelve a HN sino que te manda a la página principal de LinkedIn.
  • No es raro, es un comportamiento asqueroso. El botón de atrás debería llevarte a la página anterior.
• ¿Qué es Lean FRO?
  • https://lean-fro.org/about/
  • Lean es, por ahora, un lenguaje de programación y asistente de pruebas bastante de nicho.
    Un asistente de pruebas es básicamente una herramienta para construir demostraciones matemáticas, y verifica si una demostración es correcta del mismo modo en que un compilador verifica los tipos de un programa.
    Según entiendo, como descubrieron Curry y Howard, un lenguaje de programación general con ciertas restricciones también corresponde a un asistente de pruebas. Aquí las restricciones se sienten un poco como la forma en que Rust, en comparación con Java, obliga a seguir ciertas reglas.
  • Contexto de la organización: https://en.m.wikipedia.org/wiki/Convergent_Research
    Su asistente de pruebas/lenguaje de programación: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
  • https://lean-lang.org/lean4/doc/
  • “Su objetivo es abordar los desafíos de escalabilidad, usabilidad y automatización de pruebas (matemáticas) en el asistente de pruebas Lean”
• ¿Cómo se financia una organización sin fines de lucro de Lean para poder costear desarrolladores tan destacados? Me da curiosidad cómo suele funcionar este tipo de estructura en general.
• Parece que Apple está sufriendo una fuga de talento por varios frentes. Me pregunto qué estará pasando internamente para hacer que la gente se vaya en un momento en que el mercado laboral sigue siendo tan incierto.
  • El vigésimo millón de dólares no se siente tan grande como el decimonoveno, y cuando tus dividendos por las acciones que tienes te generan el doble de tu salario, uno empieza a preguntarse por qué no dedicarse simplemente a algo más interesante.
  • Algunas personas simplemente quieren hacer cosas geniales, y además tienen el margen para hacerlo. Rosetta 2 ya salió y es un proyecto terminado.
  • Esto habría sido cierto incluso si lo hubieras dicho en 1985. La gente talentosa tiene opciones.
  • Hace falta evidencia.
    Siempre hay gente de muchos años que se va, y al final algunos trabajos terminan sintiéndose viejos aunque no tengas otra oferta.