Pengembang Rosetta 2 Cameron Zwarich Meninggalkan Apple dan Bergabung dengan Lean FRO

• Cameron Zwarich, yang telah menangani perangkat lunak sistem level rendah di Apple selama lebih dari 15 tahun, bergabung dengan Lean FRO
• Zwarich diperkenalkan sebagai pembuat Rosetta 2, menunjukkan perpindahan pengalaman perangkat lunak sistemnya ke Lean
• Fokusnya di Lean FRO diarahkan pada peningkatan code generator Lean
• Leonardo de Moura menyambut Zwarich sebagai pengembang perangkat lunak yang luar biasa, dan berharap keahliannya akan berdampak pada ekosistem Lean
• Bergabungnya dia kali ini dapat dilihat sebagai bagian dari upaya Lean untuk melampaui alat pembuktian dan memperkuat performa eksekusi serta lapisan compiler

---

Cameron Zwarich Bergabung dengan Lean FRO

• Cameron Zwarich bergabung dengan Lean FRO
• Leonardo de Moura menyambut Zwarich sebagai pembuat Rosetta 2 sekaligus pengembang perangkat lunak yang luar biasa
• Zwarich memiliki karier lebih dari 15 tahun dengan spesialisasi di perangkat lunak sistem level rendah di Apple

Peran yang Akan Diemban di Lean

• Tugas utama Zwarich di Lean FRO adalah meningkatkan code generator Lean
• de Moura berharap keahliannya akan memberi dampak besar pada ekosistem Lean
• Postingan tersebut juga menyertakan tagar #LeanLang, #LeanProver, #LeanFRO

[GN⁺]

Komentar Hacker News

• Itu saya! Saya tidak menyangka ini akan muncul di sini, tetapi saya antusias bisa bekerja bersama Lean FRO dan orang-orang lain di komunitas Lean yang lebih luas untuk membuat Lean menjadi lebih baik.
  Latar belakang saya adalah matematika, dan saya sudah tertarik pada interactive theorem prover sejak sebelum menjadi software engineer profesional, jadi bisa melakukan pekerjaan ini secara penuh waktu rasanya hampir seperti mimpi yang menjadi kenyataan.
  • Laptop kerja saya adalah M4 MacBook Pro, jadi saya benar-benar menghargai keindahan Rosetta.
    Dari LinkedIn terlihat Anda sudah di Apple sejak 2009, dan selain satu tahun di Mozilla di tengah-tengahnya, terus berada di Apple. Saya juga melihat Anda lulusan pascasarjana matematika murni Waterloo, dan secara pribadi saya menganggap Waterloo sebagai sekolah matematika/ilmu komputer terbaik di negara kami, jadi sekarang pun di usia 40-an saya akan pergi tanpa ragu kalau diterima.
    Saya penasaran lewat jalur apa Anda bisa terlibat dalam proyek Rosetta 2. Saya juga melihat tesis pascasarjana Anda, tetapi https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... tampaknya tidak terkait dengan teori compiler.
    Saya dulu juga belajar matematika, tetapi bukan mahasiswa yang bagus; saya mengambil statistik, yang kadang saya bercandakan bukan bagian dari matematika, jadi saya tidak mengambil kelas aljabar yang serius dan sama sekali tidak memahami tesis itu.
  • Rosetta 2 adalah salah satu hasil karya teknis paling mengesankan yang pernah saya lihat seumur hidup. Saya pernah mengerjakan binary translation cukup mendalam dengan DynamoRIO, tetapi Rosetta 2 masih terasa seperti sihir.
  • Apakah Anda benar-benar pembuat Rosetta 2 itu? Saya penasaran seberapa besar timnya dan apa peran Anda.
    Rosetta 2 luar biasa, dan kalau ini pekerjaan yang dibuat oleh satu orang saja, itu sungguh mencengangkan.
  • Apakah ada buku yang bisa direkomendasikan tentang disassembly, system call, dan assembler x86/64?
    Saya penasaran apa saja yang perlu diketahui untuk membuat sesuatu secanggih Rosetta.
    Saya menduga system call dari tiap sistem host/guest diimplementasikan ulang sebagai lapisan abstraksi yang andal lalu diuji, tetapi terlalu banyak bagian yang jauh melampaui tingkat pemahaman saya.
    Apakah Anda juga membuat assembler debugger sendiri? Saya penasaran alat apa saja yang digunakan selama pengerjaan, dan apakah alat reverse engineering seperti Ghidra atau Binary Ninja juga berguna.
  • Jika Anda sudah berada di FAANG setidaknya sejak 2009, saya penasaran apakah Anda pernah pensiun atau mengambil sabbatical sekitar satu atau dua tahun.
    Dengan durasi seperti itu, kemungkinan Anda sudah menghasilkan cukup untuk pensiun dan hidup dari passive income yang mendekati gaji, dengan pajak yang jauh lebih menguntungkan.
    Saya murni penasaran bagaimana proses pengambilan keputusannya terbentuk. Kalau FAANG atau khususnya Apple terasa memuaskan, tentu saja tidak masalah; saya juga penasaran apakah ada kecemasan finansial yang sampai terasa tidak rasional, karena saya sering melihat kasus seperti itu di Blind.
• Dalam diskusi sebelumnya, nama Gary Davidian muncul; ia juga awalnya hampir sendirian melakukan pekerjaan luar biasa dalam transisi arsitektur Apple. Ada wawancaranya di arsip Computer History Museum.
  https://news.ycombinator.com/item?id=28914208
  https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
  • Kalau melihat wiki, emulator David tampaknya memakai interpreted execution, sedangkan milik Eric disebut memakai dynamic recompilation, dan versi Connectix lebih cepat, jadi sepertinya ada optimasi tambahan.
    Saya mencoba mencari source code-nya, tetapi tidak menemukan apa pun.
• Tombol kembali di LinkedIn aneh. Saat menekan kembali, bukannya kembali ke HN, malah pergi ke beranda LinkedIn.
  • Itu bukan aneh, itu perilaku yang menjijikkan. Tombol kembali seharusnya kembali ke halaman sebelumnya.
• Apa itu Lean FRO?
  • https://lean-fro.org/about/
  • Lean saat ini adalah bahasa pemrograman sekaligus proof assistant yang masih berada di ceruk niche.
    Proof assistant pada dasarnya adalah alat untuk menyusun pembuktian matematis, dan memverifikasi apakah pembuktian itu benar, sebagaimana compiler memverifikasi tipe dalam program.
    Sejauh pemahaman saya, seperti yang ditemukan Curry dan Howard, bahasa pemrograman umum dengan batasan tertentu juga berkorespondensi dengan proof assistant. Batasan di sini kira-kira mirip dengan bagaimana Rust, dibandingkan Java, memaksa kita mengikuti aturan tertentu.
  • Latar belakang organisasinya: https://en.m.wikipedia.org/wiki/Convergent_Research
    Proof assistant/bahasa pemrograman mereka: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
  • https://lean-lang.org/lean4/doc/
  • “Bertujuan menangani tantangan skalabilitas, kegunaan, dan otomasi pembuktian (matematika) dalam proof assistant Lean.”
• Bagaimana organisasi nirlaba Lean mendapatkan pendanaan sehingga mampu mempekerjakan developer sehebat ini? Saya penasaran bagaimana struktur seperti ini biasanya berjalan.
• Apple tampaknya mengalami keluarnya talenta di sana-sini. Saya penasaran apa yang terjadi di internal sampai membuat orang-orang pergi pada masa pasar kerja yang tidak pasti seperti sekarang.
  • Juta dolar ke-20 tidak terasa sebesar juta dolar ke-19, dan ketika dividen saham yang dimiliki menghasilkan 2 kali gaji tahunan, orang mulai berpikir, mengapa tidak mengerjakan sesuatu yang lebih menarik saja?
  • Sebagian orang hanya ingin melakukan hal keren, dan mereka juga punya keleluasaan untuk itu. Rosetta 2 sudah dirilis dan proyeknya sudah selesai.
  • Kalau kalimat ini diucapkan pada 1985 pun tetap benar. Orang-orang berbakat punya pilihan.
  • Perlu bukti.
    Orang-orang yang sudah lama bekerja selalu ada yang pergi, dan meski tidak ada posisi yang ditawarkan, pada akhirnya suatu pekerjaan memang bisa terasa usang.