Cameron Zwarich ผู้พัฒนา Rosetta 2 ออกจาก Apple และเข้าร่วม Lean FRO

 (linkedin.com)
1 คะแนน โดย GN⁺ 2024-12-23 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • Cameron Zwarich ซึ่งทำงานด้านซอฟต์แวร์ระบบระดับล่างที่ Apple มานานกว่า 15 ปี ได้เข้าร่วม Lean FRO
  • Zwarich ถูกแนะนำว่าเป็น ผู้สร้าง Rosetta 2 และเป็นกรณีของผู้มีประสบการณ์ด้านซอฟต์แวร์ระบบที่ย้ายมาทางฝั่ง Lean
  • จุดโฟกัสที่ Lean FRO จะอยู่ที่การ ปรับปรุงตัวสร้างโค้ด ของ Lean
  • Leonardo de Moura กล่าวต้อนรับ Zwarich ในฐานะนักพัฒนาซอฟต์แวร์ชั้นยอด และคาดว่าความเชี่ยวชาญของเขาจะส่งผลต่อ ระบบนิเวศของ Lean
  • การเข้าร่วมครั้งนี้อาจมองได้ว่าเป็นแนวโน้มที่ Lean พยายามเสริมความแข็งแกร่งไม่เพียงแค่ในฐานะเครื่องมือพิสูจน์ แต่ยังรวมถึงประสิทธิภาพการรันและชั้นคอมไพเลอร์ด้วย

Cameron Zwarich เข้าร่วม Lean FRO

  • Cameron Zwarich ได้เข้าร่วม Lean FRO
  • Leonardo de Moura กล่าวต้อนรับ Zwarich ในฐานะผู้สร้าง Rosetta 2 และนักพัฒนาซอฟต์แวร์ชั้นยอด
  • Zwarich มีประสบการณ์เชี่ยวชาญด้าน ซอฟต์แวร์ระบบระดับล่าง ที่ Apple มานานกว่า 15 ปี

บทบาทที่จะรับใน Lean

  • งานหลักของ Zwarich ที่ Lean FRO คือการปรับปรุง ตัวสร้างโค้ด ของ Lean
  • de Moura คาดว่าความเชี่ยวชาญของเขาจะสร้างผลกระทบอย่างมากต่อ ระบบนิเวศของ Lean
  • ในโพสต์มีแฮชแท็ก #LeanLang, #LeanProver, #LeanFRO ติดมาด้วย

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2024-12-23
ความคิดเห็นจาก Hacker News
  • นี่ผมเองครับ! ไม่คิดว่าจะมาโผล่ที่นี่ แต่ก็ตื่นเต้นที่จะได้ทำงานร่วมกับ Lean FRO และคนอื่น ๆ ในชุมชน Lean ที่กว้างขึ้น เพื่อทำให้ Lean ดีขึ้น
    พื้นหลังของผมคือคณิตศาสตร์ และผมสนใจ interactive theorem prover มาตั้งแต่ก่อนจะมาเป็นวิศวกรซอฟต์แวร์มืออาชีพ ดังนั้นการได้ทำงานนี้เต็มเวลาจึงใกล้เคียงกับการได้ทำฝันให้เป็นจริง
    • แล็ปท็อปที่ใช้ทำงานของผมคือ M4 MacBook Pro เลยยิ่งรู้สึกขอบคุณความงดงามของ Rosetta มากจริง ๆ
      ดูใน LinkedIn แล้วเห็นว่าเขาอยู่ Apple มาตั้งแต่ปี 2009 และนอกจากช่วงที่ไป Mozilla 1 ปี ก็อยู่ Apple มาตลอด เห็นด้วยว่าเขาจบปริญญาโท/เอกคณิตศาสตร์บริสุทธิ์จาก Waterloo และโดยส่วนตัวผมคิดว่า Waterloo เป็นโรงเรียนคณิตศาสตร์/วิทยาการคอมพิวเตอร์ที่ดีที่สุดในประเทศเรา ถึงตอนนี้จะอายุ 40 กว่าแล้ว ถ้าเขารับก็คงไปแบบไม่ลังเล
      ผมสงสัยว่าเขาเข้าไปมีส่วนร่วมกับ โปรเจกต์ Rosetta 2 ได้อย่างไร ลองดูวิทยานิพนธ์ระดับบัณฑิตศึกษาของเขาแล้ว https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... แต่ดูไม่เกี่ยวกับทฤษฎีคอมไพเลอร์เลย
      ผมเองก็เคยเรียนคณิตศาสตร์ แต่ไม่ใช่นักเรียนที่ดีนัก เรียนสถิติ ซึ่งเรามักพูดเล่นกันว่าไม่ใช่ส่วนหนึ่งของคณิตศาสตร์ เลยไม่ได้ลงเรียนวิชาพีชคณิตจริงจัง และอ่านวิทยานิพนธ์นั้นไม่เข้าใจเลย
    • Rosetta 2 เป็นหนึ่งในผลงานที่น่าประทับใจทางเทคนิคที่สุดเท่าที่เคยเห็นมาในชีวิต ผมเคยทำงาน binary translation กับ DynamoRIO ค่อนข้างลึก แต่ Rosetta 2 ก็ยังให้ความรู้สึกเหมือนเวทมนตร์อยู่ดี
    • เขาเป็น ผู้สร้างคนนั้น ของ Rosetta 2 จริง ๆ เหรอ? อยากรู้ว่าทีมใหญ่แค่ไหน และบทบาทของเขาคืออะไร
      Rosetta 2 น่าทึ่งมาก และถ้ามันเป็นงานที่คนคนเดียวทำขึ้นมาจริง ๆ ก็ต้องบอกว่าน่าทึ่งสุด ๆ
    • มีหนังสือแนะนำเกี่ยวกับ disassembly, system call และแอสเซมเบลอร์ x86/64 ไหมครับ?
      อยากรู้ว่าต้องรู้อะไรบ้างถึงจะสร้างสิ่งที่ซับซ้อนระดับ Rosetta ได้
      ผมเดาว่าน่าจะต้องนำ system call ของระบบ host/guest แต่ละฝั่งมาสร้างใหม่เป็นชั้น abstraction ที่เชื่อถือได้แล้วทดสอบ แต่มีหลายส่วนที่เกินระดับความเข้าใจของผมไปมาก
      ได้ทำ assembler debugger เองด้วยไหม? ตอนทำงานใช้เครื่องมืออะไรบ้าง และเครื่องมือ reverse engineering อย่าง Ghidra หรือ Binary Ninja มีประโยชน์ไหม
    • ถ้าอยู่ใน FAANG อย่างน้อยตั้งแต่ปี 2009 ผมสงสัยว่าเคยเกษียณหรือพักงานแบบ sabbatical สัก 1–2 ปีไหม
      ระดับนั้นน่าจะหาเงินได้พอเกษียณแล้วใช้ชีวิตด้วยรายได้แบบ passive income ใกล้เคียงเงินเดือน และภาษีก็น่าจะได้เปรียบกว่ามาก
      แค่อยากรู้ล้วน ๆ ว่ากระบวนการตัดสินใจเป็นอย่างไร ถ้าพอใจกับ FAANG หรือโดยเฉพาะ Apple อยู่แล้วก็แน่นอนว่าไม่เป็นไร และเพราะเห็นกรณีแบบนี้เยอะใน Blind เลยสงสัยว่ามีความกังวลด้านการเงินที่แทบจะไม่สมเหตุสมผลอยู่หรือเปล่า
  • ในการคุยครั้งก่อนมีชื่อ Gary Davidian โผล่มา เขาเองก็เคยทำงานที่น่าทึ่งแทบจะคนเดียวในช่วงแรกของการเปลี่ยนสถาปัตยกรรมของ Apple มีบทสัมภาษณ์อยู่ในคลังของ Computer History Museum
    https://news.ycombinator.com/item?id=28914208
    https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
    • ดูจากวิกิแล้ว emulator ของ David น่าจะใช้ interpretation ส่วนของ Eric ระบุว่าใช้ dynamic recompilation และฝั่ง Connectix เร็วกว่า จึงน่าจะมีการปรับแต่งเพิ่มเข้าไป
      พยายามหา source code แล้วแต่ไม่เจออะไรเลย
  • ปุ่มย้อนกลับ ของ LinkedIn แปลกมาก กด back แล้วไม่กลับไป HN แต่ไปหน้าแรกของ LinkedIn แทน
    • ไม่ใช่แปลก แต่เป็นพฤติกรรมที่น่าขยะแขยง ปุ่มย้อนกลับ ควรพากลับไปหน้าก่อนหน้า
  • Lean FRO คืออะไร?
    • https://lean-fro.org/about/
    • Lean ตอนนี้เป็นภาษาโปรแกรมและ proof assistant ที่ยังอยู่ในวงแคบ
      proof assistant โดยพื้นฐานคือเครื่องมือสำหรับสร้างพิสูจน์ทางคณิตศาสตร์ และตรวจสอบว่าการพิสูจน์ถูกต้องหรือไม่ เช่นเดียวกับที่คอมไพเลอร์ตรวจสอบ type ของโปรแกรม
      ตามที่ผมเข้าใจ อย่างที่ Curry กับ Howard ค้นพบ ภาษาโปรแกรมทั่วไปที่มีข้อจำกัดบางอย่างก็สอดคล้องกับ proof assistant ได้ ข้อจำกัดในที่นี้ให้ความรู้สึกคล้ายกับการที่ Rust บังคับให้ทำตามกฎบางอย่างเมื่อเทียบกับ Java
    • ภูมิหลังขององค์กร: https://en.m.wikipedia.org/wiki/Convergent_Research
      proof assistant/ภาษาโปรแกรมของพวกเขา: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
    • https://lean-lang.org/lean4/doc/
    • “มีเป้าหมายเพื่อรับมือกับความท้าทายด้าน scalability, usability และการทำ automation ของการพิสูจน์ (คณิตศาสตร์) ใน Lean proof assistant”
  • องค์กรไม่แสวงกำไรของ Lean ระดมทุนอย่างไรถึงจ้างนักพัฒนาฝีมือยอดเยี่ยมแบบนี้ได้? อยากรู้ว่าโดยทั่วไปโครงสร้างแบบนี้ทำงานอย่างไร
  • ดูเหมือน Apple กำลังเจอ การไหลออกของบุคลากรเก่ง ๆ ตามหลายจุด อยากรู้ว่าภายในเกิดอะไรขึ้นถึงทำให้คนออก ในช่วงที่ตลาดงานไม่แน่นอนแบบตอนนี้
    • เงินล้านดอลลาร์ก้อนที่ 20 ไม่ได้ให้ความรู้สึกใหญ่เท่าก้อนที่ 19 และเมื่อเงินปันผลจากหุ้นที่ถืออยู่ทำรายได้ได้เป็น 2 เท่าของเงินเดือน ก็จะเริ่มคิดว่าแล้วทำไมไม่ไปทำงานที่น่าสนใจกว่าล่ะ
    • บางคนก็แค่อยากทำ งานเจ๋ง ๆ และมีฐานะพอที่จะทำได้ Rosetta 2 เปิดตัวไปแล้ว และเป็นโปรเจกต์ที่จบไปแล้ว
    • ถ้าพูดแบบนี้ในปี 1985 ก็ยังถูกต้องอยู่ดี คนที่มีความสามารถ มีทางเลือก
    • ต้องมีหลักฐานประกอบ
      คนที่อยู่มานานออกจากงานเป็นเรื่องที่เกิดขึ้นเสมอ และแม้ไม่มีตำแหน่งใหม่เสนอมา สุดท้ายงานบางอย่างก็ย่อมเริ่มรู้สึกเก่าไปเอง