Rosetta 2 डेवलपर Cameron Zwarich ने Apple छोड़ा, Lean FRO में शामिल हुए

 (linkedin.com)
1 पॉइंट द्वारा GN⁺ 2024-12-23 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • Apple में 15 साल से अधिक समय तक low-level system software पर काम करने वाले Cameron Zwarich ने Lean FRO जॉइन किया है
  • Zwarich को Rosetta 2 के निर्माता के रूप में पेश किया गया है, और यह system software अनुभव का Lean की ओर आने का एक उदाहरण है
  • Lean FRO में उनका फोकस Lean के code generator में सुधार पर रहेगा
  • Leonardo de Moura ने Zwarich का एक उत्कृष्ट software developer के रूप में स्वागत किया और उम्मीद जताई कि उनकी विशेषज्ञता Lean ecosystem पर प्रभाव डालेगी
  • इस शामिल होने को Lean के proof tool से आगे बढ़कर execution performance और compiler layer को भी मजबूत करने की दिशा के रूप में देखा जा सकता है

Cameron Zwarich का Lean FRO में शामिल होना

  • Cameron Zwarich Lean FRO में शामिल हुए हैं
  • Leonardo de Moura ने Zwarich का Rosetta 2 के निर्माता और एक उत्कृष्ट software developer के रूप में स्वागत किया
  • Zwarich के पास Apple में 15 साल से अधिक समय तक low-level system software में विशेषज्ञता के साथ काम करने का अनुभव है

Lean में उनकी भूमिका

  • Lean FRO में Zwarich का मुख्य काम Lean के code generator को बेहतर बनाना होगा
  • de Moura को उम्मीद है कि उनकी विशेषज्ञता Lean ecosystem पर बड़ा प्रभाव डालेगी
  • पोस्ट में #LeanLang, #LeanProver, #LeanFRO हैशटैग भी शामिल हैं

संबंधित पढ़ाई

1 टिप्पणियां

 
GN⁺ 2024-12-23
Hacker News की राय
  • यह मैं ही हूँ! उम्मीद नहीं थी कि यह यहाँ आएगा, लेकिन Lean FRO और व्यापक Lean कम्युनिटी के बाकी लोगों के साथ मिलकर Lean को बेहतर बनाने के काम को लेकर उत्साहित हूँ
    मेरी पृष्ठभूमि गणित की है, और professional software engineer बनने से पहले से ही interactive theorem provers में मेरी रुचि रही है, इसलिए इस काम को full-time कर पाना लगभग सपने के सच होने जैसा है
    • मेरा work laptop M4 MacBook Pro है, इसलिए Rosetta की खूबसूरती के लिए सच में आभारी महसूस करता हूँ
      LinkedIn देखने पर पता चला कि आप 2009 से Apple में थे, और बीच में Mozilla में 1 साल बिताने के अलावा लगातार Apple में ही रहे। यह भी देखा कि आप Waterloo pure mathematics graduate school से हैं, और निजी तौर पर मैं Waterloo को हमारे देश का सबसे अच्छा math/computer science school मानता हूँ, इसलिए 40 की उम्र में भी अगर वे मुझे स्वीकार कर लें तो मैं बिना झिझक चला जाऊँगा
      जानना चाहूँगा कि आप Rosetta 2 project से किस रास्ते जुड़े। मैंने आपकी graduate thesis भी देखी, लेकिन https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... compiler theory से जुड़ी नहीं लगी
      मैंने भी पहले गणित पढ़ा था, लेकिन अच्छा छात्र नहीं था, और statistics की पढ़ाई की थी, जिसे मज़ाक में गणित का हिस्सा नहीं कहते थे, इसलिए मैंने गंभीर algebra classes नहीं लीं और वह thesis बिल्कुल समझ नहीं पाया
    • Rosetta 2 उन चीज़ों में से है जिन्हें मैंने जीवन में देखा है और जो तकनीकी रूप से सबसे प्रभावशाली लगी हैं। DynamoRIO के साथ काफी गहराई से binary translation पर काम करने के बावजूद Rosetta 2 अब भी जादू जैसा लगता है
    • क्या आप सच में Rosetta 2 के वही creator हैं? Team कितनी बड़ी थी, और आपकी भूमिका क्या थी, जानना चाहूँगा
      Rosetta 2 कमाल है, और अगर यह किसी एक व्यक्ति का काम था तो सच में हैरान कर देने वाली बात है
    • Disassembly, system calls, x86/64 assembler के बारे में कोई किताब सुझाएँगे?
      Rosetta जितनी advanced चीज़ बनाने के लिए क्या-क्या जानना पड़ता है, यह जानना चाहता हूँ
      मेरा अनुमान है कि आपने हर host/guest system के system calls को एक भरोसेमंद abstraction layer के रूप में फिर से implement करके test किया होगा, लेकिन ऐसी बहुत-सी चीज़ें हैं जो मेरी समझ से काफी आगे हैं
      क्या आपने अपना assembler debugger भी बनाया था? काम के दौरान कौन-से tools इस्तेमाल किए, और क्या Ghidra या Binary Ninja जैसे reverse engineering tools उपयोगी रहे, यह भी जानना चाहूँगा
    • अगर आप 2009 से कम-से-कम FAANG में रहे हैं, तो जानना चाहूँगा कि क्या आपने retire किया है या 1–2 साल का sabbatical कभी लिया है
      इतने समय में शायद इतना कमा लिया होगा कि retire होने पर भी salary के करीब passive income पर रहा जा सके, और taxes भी कहीं ज़्यादा अनुकूल रहे होंगे
      मुझे सच में जिज्ञासा है कि decision-making कैसे बनी। अगर FAANG या खासकर Apple संतोषजनक था तो जाहिर है ठीक है, और Blind पर ऐसे मामले बहुत देखे हैं, इसलिए यह भी जानना चाहता हूँ कि क्या irrational लगने वाली financial anxiety भी होती है
  • पिछली चर्चा में Gary Davidian नाम आया था, और उन्होंने भी Apple के architecture transition में शुरुआत में लगभग अकेले ही अद्भुत काम किया था। Computer History Museum archive में उनका interview है
    https://news.ycombinator.com/item?id=28914208
    https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
    • Wiki देखने पर लगता है कि David का emulator interpreted execution इस्तेमाल करता था, Eric वाला dynamic recompilation इस्तेमाल करता बताया गया है, और Connectix वाला अधिक तेज़ है, तो शायद उसमें और optimization की गई होगी
      Source code खोजने की कोशिश की, लेकिन कुछ नहीं मिला
  • LinkedIn का back button अजीब है। Back दबाने पर HN पर वापस नहीं जाता, बल्कि LinkedIn homepage पर चला जाता है
    • यह अजीब नहीं, घिनौना behavior है। Back button को पिछली page पर वापस जाना चाहिए
  • Lean FRO क्या है?
    • https://lean-fro.org/about/
    • Lean अभी के लिए एक niche programming language और proof assistant है
      Proof assistant मूल रूप से mathematical proofs बनाने का tool होता है, और जैसे compiler program के types verify करता है, वैसे ही यह proof सही है या नहीं verify करता है
      मेरी समझ के अनुसार, जैसा Curry और Howard ने पाया, कुछ constraints वाली सामान्य programming languages भी proof assistant से correspond करती हैं। यहाँ constraints का मतलब कुछ वैसा है जैसे Java की तुलना में Rust कुछ नियमों का पालन करवाता है
    • संगठन की पृष्ठभूमि: https://en.m.wikipedia.org/wiki/Convergent_Research
      उनका proof assistant/programming language: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
    • https://lean-lang.org/lean4/doc/
    • “Lean proof assistant में scalability, usability, और proof (mathematics) automation की चुनौतियों को हल करने का लक्ष्य रखता है”
  • Lean nonprofit संगठन funding कैसे जुटाता है कि ऐसे शानदार developers को afford कर सके? सामान्य तौर पर ऐसी structure कैसे काम करती है, यह जानना चाहता हूँ
  • ऐसा लगता है कि Apple जगह-जगह talent exodus झेल रहा है। आज जैसे uncertain job market में लोगों को छोड़कर जाने पर मजबूर करने के लिए अंदर क्या हो रहा होगा, यह जानना चाहता हूँ
    • 20वाँ million dollar, 19वें million dollar जितना बड़ा महसूस नहीं होता, और जब stock dividends से salary के 2 गुना कमाने लगते हैं, तो मन में आता है कि बस कुछ ज़्यादा interesting काम क्यों न किया जाए
    • कुछ लोग बस cool काम करना चाहते हैं, और उनके पास ऐसा करने की गुंजाइश भी होती है। Rosetta 2 पहले ही release हो चुका है और खत्म हुआ project है
    • 1985 में भी अगर यह बात कही जाती तो सही होती। talented लोगों के पास options होते हैं
    • इसके लिए evidence चाहिए
      लंबे समय से काम कर रहे लोगों का जाना हमेशा होता है, और कोई offer न भी हो तो आखिरकार कुछ काम पुराने लगने ही लगते हैं