Cameron Zwarich, nhà phát triển Rosetta 2, rời Apple để gia nhập Lean FRO

 (linkedin.com)
1 điểm bởi GN⁺ 2024-12-23 | 1 bình luận | Chia sẻ qua WhatsApp
  • Cameron Zwarich, người đã làm việc với phần mềm hệ thống cấp thấp tại Apple hơn 15 năm, đã gia nhập Lean FRO
  • Zwarich được giới thiệu là người tạo ra Rosetta 2, một trường hợp kinh nghiệm phần mềm hệ thống chuyển sang phía Lean
  • Trọng tâm công việc tại Lean FRO sẽ là cải thiện bộ sinh mã của Lean
  • Leonardo de Moura chào đón Zwarich như một nhà phát triển phần mềm xuất sắc, đồng thời kỳ vọng chuyên môn của ông sẽ tác động đến hệ sinh thái Lean
  • Việc gia nhập này có thể được xem là một xu hướng cho thấy Lean đang củng cố không chỉ vai trò công cụ chứng minh mà cả hiệu năng thực thi và tầng compiler

Cameron Zwarich gia nhập Lean FRO

  • Cameron Zwarich đã gia nhập Lean FRO
  • Leonardo de Moura chào đón Zwarich là người tạo ra Rosetta 2 và là một nhà phát triển phần mềm xuất sắc
  • Zwarich có kinh nghiệm hơn 15 năm chuyên về phần mềm hệ thống cấp thấp tại Apple

Vai trò đảm nhận tại Lean

  • Công việc chính của Zwarich tại Lean FRO là cải thiện bộ sinh mã của Lean
  • de Moura kỳ vọng chuyên môn của ông sẽ tạo ra tác động lớn đến hệ sinh thái Lean
  • Bài đăng kèm các hashtag #LeanLang, #LeanProver, #LeanFRO

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-12-23
Ý kiến trên Hacker News
  • Chính là tôi đây! Tôi không ngờ chuyện này lại được đăng ở đây, nhưng tôi rất háo hức được làm việc cùng Lean FRO và những người khác trong cộng đồng Lean rộng lớn hơn để làm cho Lean tốt hơn
    Nền tảng của tôi là toán học, và tôi đã quan tâm đến trình chứng minh định lý tương tác từ trước khi trở thành kỹ sư phần mềm chuyên nghiệp, nên việc có thể làm công việc này toàn thời gian gần như là giấc mơ thành hiện thực
    • Laptop làm việc của tôi là M4 MacBook Pro, nên tôi thật sự cảm nhận được vẻ đẹp của Rosetta
      Xem LinkedIn thì thấy anh đã ở Apple từ năm 2009, và ngoài 1 năm ở Mozilla giữa chừng thì luôn ở Apple. Tôi cũng thấy anh học cao học toán thuần túy ở Waterloo; cá nhân tôi nghĩ Waterloo là trường toán/khoa học máy tính tốt nhất ở nước tôi, nên dù giờ đã ngoài 40, nếu họ nhận thì tôi vẫn sẽ đi ngay không do dự
      Tôi tò mò anh đã đi theo con đường nào để tham gia dự án Rosetta 2. Tôi cũng xem luận văn cao học của anh, nhưng https://uwspace.uwaterloo.ca/items/4bc518ca-a846-43ce-92f0-8... có vẻ không liên quan đến lý thuyết trình biên dịch
      Trước đây tôi cũng học toán nhưng không phải sinh viên giỏi; tôi học thống kê và hay đùa rằng nó không phải một phần của toán học, nên tôi không học các lớp đại số nghiêm túc và hoàn toàn không hiểu luận văn đó
    • Rosetta 2 là một trong những thành quả kỹ thuật ấn tượng nhất tôi từng thấy trong đời. Dù tôi đã làm khá sâu về chuyển đổi nhị phân với DynamoRIO, Rosetta 2 vẫn mang cảm giác như phép màu
    • Anh có thật sự là người tạo ra Rosetta 2 không? Tôi tò mò quy mô nhóm khoảng bao nhiêu và vai trò của anh là gì
      Rosetta 2 thật đáng kinh ngạc, và nếu đây là công việc do một người duy nhất làm ra thì tôi thật sự choáng
    • Anh có cuốn sách nào muốn giới thiệu về disassembly, system call, và assembler x86/64 không?
      Tôi tò mò cần biết những gì để tạo ra thứ tinh vi như Rosetta
      Tôi đoán các anh đã triển khai lại và kiểm thử system call của từng hệ thống host/guest thành một lớp trừu tượng đáng tin cậy, nhưng có quá nhiều phần vượt xa mức hiểu biết của tôi
      Các anh có tự làm assembler debugger không? Tôi cũng tò mò các anh đã dùng những công cụ nào trong quá trình làm việc, và liệu các công cụ reverse engineering như Ghidra hay Binary Ninja có hữu ích không
    • Nếu đã ở FAANG ít nhất từ năm 2009, tôi tò mò liệu anh từng nghỉ hưu hoặc nghỉ sabbatical khoảng 1–2 năm chưa
      Với chừng đó thời gian, có khả năng anh đã kiếm đủ để nghỉ hưu mà vẫn sống bằng thu nhập thụ động gần mức lương, và thuế có lẽ cũng thuận lợi hơn nhiều
      Tôi thuần túy tò mò quá trình ra quyết định đã hình thành như thế nào. Nếu FAANG, đặc biệt là Apple, khiến anh hài lòng thì dĩ nhiên là ổn, và vì tôi đã thấy nhiều trường hợp như vậy trên Blind nên cũng tò mò liệu có sự bất an tài chính đến mức gần như phi lý không
  • Trong một cuộc thảo luận trước đây có nhắc đến cái tên Gary Davidian; ông ấy cũng từng gần như một mình làm được công việc đáng kinh ngạc trong giai đoạn chuyển đổi kiến trúc của Apple. Có một cuộc phỏng vấn trong kho lưu trữ của Computer History Museum
    https://news.ycombinator.com/item?id=28914208
    https://youtu.be/MVEKt_H3FsI?si=BbRRV51ql1V6DD4r
    • Nhìn trên wiki thì emulator của David có vẻ dùng diễn dịch để chạy, còn của Eric được nói là dùng biên dịch lại động; phía Connectix thì nhanh hơn nên có vẻ đã tối ưu thêm
      Tôi đã thử tìm mã nguồn nhưng không tìm thấy gì
  • Nút quay lại của LinkedIn rất kỳ lạ. Bấm quay lại không đưa về HN mà lại chuyển đến trang chủ LinkedIn
    • Không phải kỳ lạ, mà là hành vi kinh tởm. Quay lại thì phải quay về trang trước đó
  • Lean FRO là gì?
    • https://lean-fro.org/about/
    • Lean hiện là một ngôn ngữ lập trình kiêm trợ lý chứng minh còn khá ngách
      Trợ lý chứng minh về cơ bản là công cụ để xây dựng chứng minh toán học, và kiểm tra chứng minh có đúng hay không giống như compiler kiểm tra kiểu của chương trình
      Theo tôi hiểu, như Curry và Howard đã phát hiện, các ngôn ngữ lập trình thông thường với một số ràng buộc nhất định cũng tương ứng với trợ lý chứng minh. Những ràng buộc ở đây có cảm giác giống như cách Rust buộc ta tuân theo một số quy tắc nhất định so với Java
    • Bối cảnh tổ chức: https://en.m.wikipedia.org/wiki/Convergent_Research
      Trợ lý chứng minh/ngôn ngữ lập trình của họ: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
    • https://lean-lang.org/lean4/doc/
    • “Mục tiêu là giải quyết các thách thức về khả năng mở rộng, tính dễ dùng, và tự động hóa chứng minh (toán học) trong trợ lý chứng minh Lean”
  • Tổ chức phi lợi nhuận Lean huy động vốn bằng cách nào để có thể chi trả cho những nhà phát triển xuất sắc như vậy? Tôi tò mò nhìn chung mô hình kiểu này vận hành ra sao
  • Có vẻ Apple đang bị chảy máu nhân tài ở nhiều nơi. Tôi tò mò bên trong đang xảy ra chuyện gì khiến mọi người rời đi trong thời điểm thị trường tuyển dụng bất định như hiện nay
    • Triệu đô thứ 20 không còn tạo cảm giác lớn như triệu đô thứ 19, và khi cổ tức từ cổ phiếu nắm giữ đem lại gấp đôi lương thì người ta bắt đầu nghĩ vì sao mình không làm việc gì thú vị hơn
    • Một số người đơn giản là muốn làm những việc hay ho, và họ cũng có điều kiện để làm vậy. Rosetta 2 đã ra mắt và là dự án đã kết thúc
    • Nói câu này vào năm 1985 cũng vẫn đúng. Người tài luôn có lựa chọn
    • Cần có bằng chứng
      Người làm lâu năm rời đi là chuyện luôn xảy ra, và ngay cả khi không có vị trí mới được đề nghị, cuối cùng một công việc nào đó cũng sẽ bắt đầu có cảm giác cũ kỹ