Rosetta 2 geliştiricisi Cameron Zwarich, Apple'dan ayrılıp Lean FRO'ya katıldı

• Apple'da 15 yılı aşkın süredir düşük seviye sistem yazılımı üzerinde çalışan Cameron Zwarich, Lean FRO'ya katıldı
• Zwarich, Rosetta 2'nin yaratıcısı olarak tanıtılıyor ve bu, sistem yazılımı deneyiminin Lean tarafına taşındığı bir örnek
• Lean FRO'daki odağı, Lean'in kod üreticisini iyileştirmek olacak
• Leonardo de Moura, Zwarich'i üstün bir yazılım geliştirici olarak karşılıyor ve uzmanlığının Lean ekosistemi üzerinde etkili olmasını bekliyor
• Bu katılım, Lean'in kanıtlama aracının ötesine geçerek çalışma zamanı performansı ve derleyici katmanını da güçlendirme yönündeki eğilimin parçası olarak görülebilir

---

Cameron Zwarich'in Lean FRO'ya katılması

• Cameron Zwarich, Lean FRO'ya katıldı
• Leonardo de Moura, Zwarich'i Rosetta 2'nin yaratıcısı ve üstün bir yazılım geliştiricisi olarak karşıladı
• Zwarich, Apple'da 15 yılı aşkın süre düşük seviye sistem yazılımı konusunda uzmanlaşmış bir kariyere sahip

Lean'de üstleneceği rol

• Lean FRO'da Zwarich'in ana görevi, Lean'in kod üreticisini iyileştirmek olacak
• de Moura, onun uzmanlığının Lean ekosistemi üzerinde büyük bir etki yaratmasını bekliyor
• Gönderide #LeanLang, #LeanProver, #LeanFRO etiketleri de yer alıyor

[GN⁺]

Hacker News yorumları

• Bu benim! Bunun buraya düşeceğini bilmiyordum ama Lean FRO ve daha geniş Lean topluluğundaki diğer insanlarla birlikte Lean’i daha iyi hale getirmek için çalışacak olmaktan heyecan duyuyorum
  Geçmişim matematik; profesyonel bir yazılım mühendisi olmadan önce de etkileşimli teorem ispatlayıcılar ile ilgileniyordum, bu yüzden bunu tam zamanlı yapabilmek neredeyse bir hayalin gerçekleşmesi gibi
  • İş dizüstü bilgisayarım M4 MacBook Pro, bu yüzden Rosetta’nın güzelliğini gerçekten takdir ediyorum
    LinkedIn’e bakınca 2009’dan beri Apple’da olduğunu, arada Mozilla’da geçirdiği 1 yıl dışında hep Apple’da kaldığını gördüm. Waterloo’da saf matematik yüksek lisansı yaptığını da gördüm; kişisel olarak Waterloo’nun ülkemizdeki en iyi matematik/bilgisayar bilimi okulu olduğunu düşünüyorum, bu yüzden 40’lı yaşlarımda olmama rağmen kabul ederlerse hiç tereddüt etmeden giderdim
    Rosetta 2 projesine nasıl dahil olduğunuzu merak ediyorum. Yüksek lisans tezine de baktım ama https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... derleyici teorisiyle ilgili görünmüyordu
    Ben de zamanında matematik okudum ama iyi bir öğrenci değildim; istatistik yaptım ve şaka yollu bunun matematiğin bir parçası olmadığını söylerdim, bu yüzden ciddi bir cebir dersi almadım ve o tezi hiç anlayamadım
  • Rosetta 2, hayatımda gördüğüm en teknik açıdan etkileyici işlerden biri. DynamoRIO ile oldukça derin ikili çeviri çalışmaları yapmış olmama rağmen Rosetta 2 hâlâ sihir gibi geliyor
  • Gerçekten Rosetta 2’nin o geliştiricisi misiniz? Ekip ne kadardı ve sizin rolünüz neydi, merak ediyorum
    Rosetta 2 inanılmaz; eğer bu tek kişinin yaptığı bir işse gerçekten hayret verici
  • Disassembly, sistem çağrıları ve x86/64 assembler hakkında önerebileceğiniz kitaplar var mı?
    Rosetta kadar gelişmiş bir şey yapmak için neleri bilmek gerektiğini merak ediyorum
    Her host/guest sistemin sistem çağrılarını güvenilebilir bir soyutlama katmanı olarak yeniden uygulayıp test ettiğinizi tahmin ediyorum ama kavrayışımın çok ötesinde kalan çok fazla nokta var
    Kendi assembler debugger’ınızı da yaptınız mı? Çalışırken hangi araçları kullandığınızı, Ghidra veya Binary Ninja gibi tersine mühendislik araçlarının faydalı olup olmadığını da merak ediyorum
  • 2009’dan beri en azından FAANG içindeyseniz, emekli olmayı ya da 1-2 yıllık bir ara vermeyi hiç düşündünüz mü merak ediyorum
    Bu kadar sürede emekli olsanız bile maaşa yakın düzeyde pasif gelirle yaşayacak kadar kazanmış olabilirsiniz ve vergisel açıdan da çok daha avantajlı olurdu diye düşünüyorum
    Kararınızın nasıl şekillendiğini tamamen merak ediyorum. FAANG ya da özellikle Apple sizin için tatmin ediciyse elbette sorun yok, ama Blind’de böyle çok şey gördüğüm için bunun mantıksız denecek düzeyde bir finansal güvensizlik olup olmadığını da merak ediyorum
• Önceki bir tartışmada Gary Davidian adı geçmişti; o da Apple’ın mimari geçişlerinde başlangıçta neredeyse tek başına inanılmaz işler yapmıştı. Computer History Museum arşivinde bir röportajı var
  https://news.ycombinator.com/item?id=28914208
  https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
  • Wiki’ye göre David’in emülatörü yorumlamalı yürütme kullanıyormuş, Eric’inki ise dinamik yeniden derleme kullanıyormuş; Connectix tarafı daha hızlı olduğuna göre daha fazla optimizasyon yapılmış gibi görünüyor
    Kaynak kodunu bulmaya çalıştım ama hiçbir şey bulamadım
• LinkedIn’in geri düğmesi tuhaf davranıyor. Geri’ye basınca HN’ye dönmek yerine LinkedIn ana sayfasına gidiyor
  • Tuhaf değil, iğrenç bir davranış. Geri önceki sayfaya dönmelidir
• Lean FRO nedir?
  • https://lean-fro.org/about/
  • Lean, şu an için niş sayılabilecek bir programlama dili ve ispat asistanıdır
    İspat asistanı temelde matematiksel ispatlar kurmaya yarayan bir araçtır ve derleyicinin bir programın tiplerini doğrulaması gibi, ispatın doğru olup olmadığını doğrular
    Benim anladığım kadarıyla Curry ve Howard’ın gösterdiği gibi, belirli kısıtları olan genel amaçlı programlama dilleri de ispat asistanlarına karşılık gelir. Buradaki kısıtlar da, Java’ya kıyasla Rust’ın bazı kuralları zorunlu kılması gibi düşünülebilir
  • Kurumsal arka plan: https://en.m.wikipedia.org/wiki/Convergent_Research
    Bunların ispat asistanı/programlama dili: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
  • https://lean-lang.org/lean4/doc/
  • “Lean ispat asistanında ölçeklenebilirlik, kullanılabilirlik ve ispat (matematik) otomasyonu sorunlarını ele almayı amaçlıyor”
• Lean kâr amacı gütmeyen kuruluşu, bu kadar yetenekli geliştiricileri karşılayacak finansmanı nasıl sağlıyor? Genel olarak bu yapının nasıl işlediğini merak ediyorum
• Apple’ın çeşitli yerlerde yetenek kaybı yaşadığı görülüyor. İş piyasasının şu an bu kadar belirsiz olduğu bir dönemde insanların ayrılmasına yol açacak içeride ne oluyor, merak ediyorum
  • 20. milyon dolar, 19. milyon dolar kadar büyük hissettirmiyor; elde tuttuğunuz hisselerin temettüsü maaşınızın iki katını kazandırıyorsa, neden gidip daha ilginç bir iş yapmayayım diye düşünüyorsunuz
  • Bazı insanlar sadece havalı işler yapmak istiyor ve bunu yapabilecek rahatlığa da sahip. Rosetta 2 zaten çıktı ve tamamlanmış bir proje
  • Bunu 1985’te de söyleseniz doğru olurdu. Yetenekli insanların seçenekleri vardır
  • Buna dair kanıt lazım
    Uzun süre kalan insanların ayrılması her zaman olur; ortada başka bir teklif olmasa bile zamanla bazı işler eski hissettirmeye başlar