Cameron Zwarich, desenvolvedor do Rosetta 2, deixa a Apple e se junta à Lean FRO

 (linkedin.com)
1 pontos por GN⁺ 2024-12-23 | 1 comentários | Compartilhar no WhatsApp
  • Cameron Zwarich, que trabalhou por mais de 15 anos com software de sistemas de baixo nível na Apple, juntou-se à Lean FRO
  • Zwarich é apresentado como o criador do Rosetta 2, um caso de experiência em software de sistemas migrando para o ecossistema Lean
  • Na Lean FRO, o foco será a melhoria do gerador de código do Lean
  • Leonardo de Moura dá as boas-vindas a Zwarich como um desenvolvedor de software excepcional e espera que sua especialidade tenha impacto no ecossistema Lean
  • Essa contratação pode ser vista como parte do movimento do Lean para ir além das ferramentas de prova e também fortalecer desempenho de execução e a camada de compilador

Cameron Zwarich se junta à Lean FRO

  • Cameron Zwarich juntou-se à Lean FRO
  • Leonardo de Moura deu as boas-vindas a Zwarich como o criador do Rosetta 2 e um desenvolvedor de software excepcional
  • Zwarich tem mais de 15 anos de experiência especializado em software de sistemas de baixo nível na Apple

Papel que assumirá no Lean

  • Na Lean FRO, a principal função de Zwarich será melhorar o gerador de código do Lean
  • de Moura espera que sua especialidade tenha grande impacto no ecossistema Lean
  • A publicação também inclui as hashtags #LeanLang, #LeanProver, #LeanFRO

Leituras relacionadas

1 comentários

 
GN⁺ 2024-12-23
Comentários do Hacker News
  • Sou eu mesmo! Não esperava ver isso aparecer aqui, mas estou animado por trabalhar para tornar o Lean melhor junto com o Lean FRO e outras pessoas da comunidade Lean em geral
    Minha formação é em matemática, e eu já me interessava por assistentes interativos de prova antes de me tornar engenheiro de software profissional, então poder fazer isso em tempo integral é quase como realizar um sonho
    • Meu notebook de trabalho é um M4 MacBook Pro, então sou realmente grato pela beleza do Rosetta
      Pelo LinkedIn, vi que ele estava na Apple desde 2009 e, tirando um ano na Mozilla no meio do caminho, ficou o tempo todo na Apple. Também vi que ele fez pós-graduação em matemática pura em Waterloo e, pessoalmente, acho Waterloo a melhor escola de matemática/ciência da computação do nosso país, então mesmo agora, já na casa dos 40, eu iria sem hesitar se me aceitassem
      Fico curioso sobre como ele acabou entrando no projeto Rosetta 2. Até fui olhar a dissertação dele https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8..., mas não parecia ter relação com teoria de compiladores
      Eu também estudei matemática no passado, mas não era um bom aluno; fiz estatística, que eu brincava não ser parte da matemática, então nunca cursei álgebra séria e também não entendi nada daquela dissertação
    • Rosetta 2 é uma das coisas tecnicamente mais impressionantes que já vi na vida. Já trabalhei relativamente a fundo com tradução binária usando DynamoRIO, e mesmo assim o Rosetta 2 ainda parece mágica
    • É realmente o criador do Rosetta 2? Quão grande era a equipe e qual foi exatamente o seu papel?
      O Rosetta 2 é impressionante, mas se isso foi trabalho de uma única pessoa, então é sinceramente espantoso
    • Alguma recomendação de livros sobre desmontagem, chamadas de sistema e assembly x86/64?
      Queria entender o que é preciso saber para construir algo tão sofisticado quanto o Rosetta
      Suponho que vocês tenham reimplementado e testado as chamadas de sistema de cada sistema host/guest como uma camada de abstração confiável, mas há coisa demais aqui que está muito além do meu nível de compreensão
      Você também criou um depurador de assembly próprio? Quais ferramentas usou durante o trabalho, e se ferramentas de engenharia reversa como Ghidra ou Binary Ninja foram úteis
    • Se você está em uma FAANG pelo menos desde 2009, fico curioso se já se aposentou ou tirou um sabático de 1 a 2 anos
      A essa altura, parece possível que você tenha ganhado o bastante para se aposentar e viver de renda passiva em um nível próximo ao salário, e provavelmente com impostos bem mais favoráveis
      Tenho curiosidade genuína sobre como essa decisão foi formada. Se FAANG, ou especialmente a Apple, era satisfatória, tudo bem, claro, mas como vejo muito esse tipo de coisa no Blind, também me pergunto se existe uma insegurança financeira irracional aí
  • Em discussões antigas, apareceu o nome Gary Davidian, e ele também fez um trabalho incrível quase sozinho no começo de uma transição de arquitetura da Apple. Há uma entrevista no arquivo do Computer History Museum
    https://news.ycombinator.com/item?id=28914208
    https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
    • Pela Wikipédia, parece que o emulador do David usava interpretação, enquanto o do Eric usava recompilação dinâmica, e o da Connectix parece ter sido ainda mais rápido, então imagino que tivesse mais otimizações
      Tentei encontrar o código-fonte, mas não achei nada
  • O botão de voltar do LinkedIn é estranho. Mesmo apertando voltar, ele não retorna para o HN, mas vai para a página inicial do LinkedIn
    • Não é estranho, é um comportamento nojento. Voltar deve levar de volta à página anterior
  • O que é Lean FRO?
    • https://lean-fro.org/about/
    • Lean é, por enquanto, uma linguagem de programação e assistente de provas de nicho
      Um assistente de provas é basicamente uma ferramenta para construir provas matemáticas, e verifica se a prova está correta do mesmo jeito que um compilador verifica os tipos de um programa
      Pelo que entendi, como Curry e Howard descobriram, linguagens de programação gerais com certas restrições também correspondem a assistentes de prova. Aqui, essas restrições lembram um pouco como Rust, em comparação com Java, força você a seguir certas regras
    • Contexto da organização: https://en.m.wikipedia.org/wiki/Convergent_Research
      O assistente de provas/linguagem de programação deles: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
    • https://lean-lang.org/lean4/doc/
    • “O objetivo é enfrentar os desafios de escalabilidade, usabilidade e automação de provas (matemáticas) no assistente de provas Lean”
  • Como uma organização sem fins lucrativos do Lean consegue financiamento para bancar desenvolvedores tão excelentes? Fico curioso sobre como esse tipo de estrutura costuma funcionar
  • Parece que a Apple está sofrendo uma saída de talentos em vários lugares. Fico curioso sobre o que está acontecendo internamente para fazer as pessoas saírem num momento em que o mercado de trabalho é incerto como agora
    • O vigésimo milhão de dólares não impacta tanto quanto o décimo nono, e quando os dividendos das ações que você já tem passam a render o dobro do seu salário, você começa a pensar por que não fazer algo mais interessante
    • Algumas pessoas simplesmente querem fazer coisas legais, e têm margem para isso. O Rosetta 2 já foi lançado e é um projeto concluído
    • Isso teria sido verdade mesmo se você dissesse isso em 1985. Pessoas talentosas têm opções
    • Isso precisa de fundamento
      Sempre há pessoas de longa data indo embora, e mesmo sem uma oferta concreta, eventualmente algum trabalho começa a parecer velho