บันทึกบางประการเกี่ยวกับ mutable aliasing และการตรวจสอบชนิดใน Rust

ไม่มีเนื้อหาสำหรับสรุป

[GN⁺]

ความคิดเห็นใน Hacker News

• เป็นบทความที่ดี ในฐานะคนที่เคยทำ การพิสูจน์ความถูกต้องของโปรแกรม มาก่อน Rust ดูเหมือนเป็นภาษาสมัยใหม่ที่มีประโยชน์ที่สุดสำหรับการนำเทคนิคเชิงรูปนัยมาใช้
  กฎของ Rust ช่วยตัดกรณีจำนวนมากที่ทำให้ทำให้เป็นรูปนัยได้ยากออกไป ปัญหาใหญ่ที่เหลือคือ การวิเคราะห์ deadlock ในมุมของเธรดกับในมุมของ Rc/การยืม ซึ่งสองอย่างนี้ค่อนข้างเทียบเท่ากัน ถ้า Rust มีการวิเคราะห์ deadlock แบบสถิติก็น่าจะทำให้มี dereference pointer ที่ปลอดภัยได้ และถ้าพิสูจน์ได้ว่า borrow/upgrade ทุกครั้งจะไม่ล้มเหลว ก็อาจตัดการนับจำนวนอ้างอิงส่วนใหญ่ออกได้ แบบนั้นก็จะได้ interior mutability ฟรีในกรณีที่ทำได้
  ปัญหาใหญ่ของตัวพิสูจน์ทฤษฎีบทคือมักถูกสร้างโดยคนที่ชอบพิสูจน์ทฤษฎีบท เลยหมกมุ่นกับความเป็นรูปนัยจนไม่ค่อยตรงกับความรู้สึกของโปรแกรมเมอร์และการออกแบบ UI ภาระการพิสูจน์ส่วนใหญ่จัดการได้ด้วย SAT solver แต่ปัญหายาก ๆ ต้องใช้เครื่องมือที่หนักกว่านั้น Coq ต้องทำด้วยมือมากเกินไป และผู้เขียนมองว่า ACL2 เป็นเชิงฟังก์ชันมากเกินไป machine learning อาจช่วยนำทางทิศทางของตัวพิสูจน์ทฤษฎีบทได้ อาจยากที่จะให้มันพิสูจน์แทนทั้งหมด แต่การอนุมานแผนการพิสูจน์จากโค้ดที่มี control flow และการใช้ข้อมูลคล้ายกันโดยรวมก็ดูเป็นไปได้

  • F* ใกล้เคียงกับภาษาระดับตำนานที่พิสูจน์ให้อัตโนมัติ ใช้ SMT solver ที่ทรงพลังกว่า SAT และถ้าการแก้อัตโนมัติล้มเหลวก็ยังพิสูจน์ด้วยมือได้
    รูทีนเข้ารหัสของ Firefox และ Wireguard ไม่ได้เขียนด้วย Rust แต่เขียนด้วย F* หรือให้แม่นยำกว่านั้นคือ Low* ซึ่งเป็น DSL ระดับต่ำที่ฝังอยู่ใน F* และได้รับการพิสูจน์ครบถ้วนแล้ว
    https://project-everest.github.io/
    https://mitls.org/
  • เห็นด้วย แต่คิดว่า Lean กำลังก้าวหน้าอย่างมากในประสบการณ์ผู้ใช้ของการตรวจสอบการพิสูจน์ทฤษฎีบทแบบโต้ตอบได้ ด้วยความสามารถด้านเมตาโปรแกรมมิงที่หลากหลาย
    ปัญหาเวลานำเครื่องมือแบบนี้ไปใช้กับการตรวจสอบภาษาอื่นอย่าง Rust คือการพิสูจน์ไม่ได้เขียนด้วยภาษาเป้าหมาย ทำให้นักพัฒนาต้องเรียนสองภาษา จากประสบการณ์การเขียน Creusot การทำงานกับ Verus และ Aeneas และประสบการณ์ในแล็บ Why3 จึงได้คิดต่อว่า “Rust ที่ออกแบบโดยคำนึงถึงการตรวจสอบ” ควรมีหน้าตาอย่างไร ถ้าสร้างภาษานั้นขึ้นมาตั้งแต่ต้น ก็อาจทำให้ตรวจสอบได้ง่ายกว่า Rust แบบเป็นลำดับขั้น โดยเฉพาะในส่วนที่ยากของการพิสูจน์
  • สาย Coq/Agda/Lean น่าจะเป็นผู้ชนะในโลกการพิสูจน์ การโต้ตอบเป็นโมเดลที่ดีมากในแง่ feedback loop และก็เป็นระบบที่มีอยู่แล้วและใช้งานได้จริง
    สิ่งที่น่าเสียดายที่สุดในความสามารถพื้นฐานคือยังไม่มีอะไรประมาณ “ช่วยรัน quickcheck กับ proof ของฉันหน่อย” เวลามีโค้ดอยู่แล้วแต่พยายามพิสูจน์คุณสมบัติที่จริง ๆ ไม่เป็นความจริง ก็มักลงเอยด้วยการปวดหัวว่าทำไมพิสูจน์ไม่ผ่าน ถ้าระหว่างพิสูจน์ไปถึงสถานะที่ไม่สมเหตุสมผล แล้วมีคำสั่งอย่าง “ลองสร้าง counterexample ตรงนี้” ที่คืนตัวอย่างโต้แย้งกลับมาได้ก็คงดี การพิสูจน์พึ่งพาเส้นทางอย่างมากและโดยทั่วไปไม่ง่าย แต่เครื่องมือพวกนี้ดูใกล้เคียงความยอดเยี่ยมมาก กระบวนการพยายามพิสูจน์โค้ดควรสะท้อนด้วยว่าโค้ดนั้นอาจมีบั๊กได้
  • แนวคิดที่ให้ machine learning มาช่วยนำทางตัวพิสูจน์ทฤษฎีบทน่าสนใจมาก ถ้าระบบ machine learning เดาถูก ก็จะพาไปสู่ proof ที่ใช้ได้จริงและได้ประโยชน์มาก ถ้าเดาผิดก็ไม่ได้เสียหายมาก
    ตัวพิสูจน์จะไม่สร้าง proof ที่ผิดขึ้นมา แค่ล้มเหลวในการหา proof ที่ถูกต้องเท่านั้น คิดว่าแอปพลิเคชันของ machine learning ที่มีคุณสมบัติแบบนี้ไม่ได้มีมากนัก
  • ไม่ใช่ผู้เชี่ยวชาญด้าน formal verification แต่คิดว่า lock ในความหมายดั้งเดิมไม่ได้ช่วยอะไรนัก ไม่มีคอมไพเลอร์ไหนให้สิ่งที่มีประโยชน์จริงจังเกี่ยวกับ lock ได้ และสุดท้ายก็ต้องยอมรับความเสี่ยงแล้วอยู่กับมัน
    ที่จริงแล้วใน Rust ทั้ง lock และ reference count เป็นโครงสร้างขณะรันไทม์ Arc ทำลายโมเดล RAII ของ Rust ไปมาก ถึงขั้นต้องถอด scoped thread ออก เพราะ destructor จำเป็นต้องรันก่อนออกจากสโคป global reference count มีปัญหาเรื่องวงจรและการรั่วไหล เลยกลายเป็นปัญหาแบบ global อีกครั้ง แม้จะลบออกทั้งหมดได้ยาก แต่ก็เชื่อว่าการกักมันไว้ในสโคปแบบ arena น่าจะดีกว่า ส่วน lock นั้นดูเหมือนต้องใช้โครงสร้างข้อมูลแบบไม่สมมาตรอย่าง channel ใน Go สามารถแยก channel เป็นฝั่งส่งกับฝั่งรับได้ และตั้ง defer close(ch) ใน goroutine ฝั่งส่งได้ ต่อให้เกิด panic ก็ยังรับประกันได้ว่าจะรันเมื่อส่วนที่เหลือของเธรดจบลง ไม่จำเป็นต้องเป็น channel ก็ได้ แต่ถ้าแยกบทบาทอ่าน-เขียน/ผู้ผลิต-ผู้บริโภคออกจากกัน การให้เหตุผลจะง่ายขึ้นมากและน่าจะช่วยต่อการวิเคราะห์เชิงรูปนัยด้วย

• ชอบที่เรื่องนี้เริ่มจากการอ้างถึงบทความของ Hoare ราวปี 1973 แล้วตอนนี้ก็ต่อเนื่องมาถึงบทความชิ้นที่สองแล้ว เดิมทีฉันเคยเขียนคอมเมนต์ยาวไว้ในเธรด HN ของบทความ boat ว่าการโน้มการอ้างถึงนั้นไปในมุมมองแบบ Rust เป็นศูนย์กลาง นั้นก็พอเข้าใจได้จากพื้นเพของ boat แต่เป็นการทำให้ขอบเขตของคำวิจารณ์ Hoare แคบลงอย่างประดิษฐ์เกินไป
  ตอนนี้ Grayson ใช้ชิ้นส่วนที่แคบลงนั้นเป็นจุดตั้งต้นเพื่อพูดถึงบางพื้นที่และจุดออกแบบที่น่าสนใจของ Rust ฉันยังคิดว่าคอมเมนต์เดิมของฉันถูกต้อง แต่การถกเถียงที่ต่อเนื่องมาจากบทความของ Grayson ก็มากพอจะชดเชยความไม่พอใจเชิงเทคนิคที่มีต่อบทความต้นทาง

  • ราวกลางทศวรรษ 1990 Hoare เองก็ดูจะตระหนักแล้วว่าอาจมีบางอย่างผิดพลาดอยู่ในรากฐานของ แนวทางที่ยึดความสมบูรณ์เชิงทฤษฎีเป็นศูนย์กลาง แบบยุค 1970: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
    หลังจากนั้น เมื่อมีเทคนิคแบบไม่สมบูรณ์เชิงทฤษฎีที่ก้าวหน้ากว่าการทดสอบแบบง่าย ๆ ปรากฏขึ้น ฉันมองว่าวิธีแบบไม่สมบูรณ์เชิงทฤษฎีก็เริ่มแซงหน้าวิธีแบบสมบูรณ์เชิงทฤษฎีไปแล้ว
  • สำหรับคนที่พลาดบทความก่อนหน้า ลิงก์คอมเมนต์นี้น่าจะช่วยได้: https://news.ycombinator.com/item?id=40355876
  • ปี 1973 คือเมื่อ 50 ปีก่อน ซึ่งเท่ากับหนึ่งช่วงชีวิตการทำงานของผู้เชี่ยวชาญคนหนึ่ง Hoare เข้าใกล้คำตอบมากจริง ๆ
    เขาพบปัญหาแล้ว และเมื่อมองย้อนหลัง วิธีแก้ที่บังคับ shared XOR mutability ด้วยระบบชนิดก็ดูเหมือนเป็นเพียงก้าวเล็ก ๆ เท่านั้น ถ้าในตอนนั้นรู้ว่าก้าวเล็ก ๆ นั้นคือคำตอบ ก็คงลดความทุกข์ทรมานมหาศาลตลอด 50 ปีลงได้มาก
  • นี่คือสิ่งที่เดิมฉันเขียนไว้เกี่ยวกับการอ้างบทความของ Hoare โดย boat หลังจากการอ้าง Hoare ครั้งแรกและบทนำสั้น ๆ ผู้เขียนกล่าวว่า “สิ่งที่ Tony Hoare กำลังพูดถึงเมื่อเขาบอกว่า references are like jumps คือปัญหาของสถานะที่เปลี่ยนแปลงได้และมี alias” withoutboats เป็นนักพัฒนา Rust ที่มีชื่อเสียง ดังนั้นการตีความแบบนี้จึงไม่น่าแปลกใจ
    แต่ฉันไม่คิดว่าตัวข้อความอ้างเองจะช่วยตอกย้ำมุมมองนั้นนัก จะมองได้ว่าเป็นความพยายามหยิบคำคร่ำครวญของ Hoare ที่กว้างกว่านั้นเกี่ยวกับการมีอยู่เชิงอรรถศาสตร์ของ reference เอง มาปรับใช้กับโมเดลสถานะเปลี่ยนแปลงได้แบบไม่ alias ของ Rust เพื่อหลบเลี่ยงปัญหา อย่างไรก็ดี นี่ใกล้เคียงกับการซ่อมเพียงชิ้นแคบ ๆ ของปัญหาใหญ่กว่า แล้วบอกว่าปัญหาทั้งหมดหายไปแล้ว ส่วนที่ถูกละไว้ โดยเฉพาะต้นของหัวข้อ “Variables” และตัวอย่าง ALGOL 68 เอนเอียงอย่างชัดเจนกว่ามากไปทางที่ว่า Hoare กำลังวิจารณ์ไม่ใช่แค่สถานะที่เปลี่ยนแปลงได้ แต่รวมถึง แนวคิดเชิงอรรถศาสตร์ของ reference เอง ด้วย ฉันยอมรับว่า Rust เป็นความพยายามที่จะทำให้ปัญหาบางส่วนเชื่องลง แต่ไม่คิดว่ามีภาษาใด “แก้” ปัญหานี้ได้แล้ว

• ฉันไม่ค่อยเข้าใจว่าทำไมบทความนี้ถึงได้รับคำชมมากขนาดนี้ รู้สึกเหมือนเอาหลายสาขาของ program analysis มารวมกลบในย่อหน้าเดียว ฉันชอบ Graydon และเคารพมุมมองของเขา แต่ย่อหน้านี้ทำให้เรื่องง่ายเกินไป
  คำอธิบายทำนองว่าภาษาที่มี GC ไม่ได้มีการรองรับการอนุมานเชิงเฉพาะที่อย่างเข้มแข็งนั้นเป็นการตั้งหุ่นฟาง มีภาษาอย่าง Pony ที่ใช้ GC แต่ก็มี region อยู่ในระบบชนิด นอกจากนี้ยังมีทั้งสาขาของ pointer analysis และ escape analysis ที่อนุมานความเป็นเอกเทศและตัดสินได้ว่า reference สองตัวอาจเป็น alias กันหรือไม่ แกนสำคัญของ static typing เองก็คือเทคนิคการใช้ class และ field เพื่อแบ่ง heap ออกเป็นส่วนที่ไม่ alias กัน ไม่ได้กำลังพูดถึง JavaScript และไม่ควรทำเหมือนว่า Java/C#/Scala และภาษา GC อีกมากมายไม่มีการอนุมานเชิงเฉพาะที่เกี่ยวกับสถานะที่เปลี่ยนแปลงได้

  • ในกรณีทั่วไป เราไม่สามารถทำสิ่งนี้ให้สมบูรณ์แบบโดยอัตโนมัติได้ และในทางปฏิบัติก็ต้องการบางอย่างที่ค่อนข้างคล้ายกับ separation logic จริง ๆ ความหมายเชิงอรรถศาสตร์ของ borrow checker ใน Rust ก็อาจมองได้ว่าเป็น separation logic แบบย่อรูปชนิดหนึ่ง
    class และ field ไม่ได้ให้การอนุมานเชิงเฉพาะที่แบบสมบูรณ์เกี่ยวกับสถานะที่เปลี่ยนแปลงได้ เพราะ class/object A อาจไปพึ่งพาสถานะที่เปลี่ยนแปลงได้ของ class/object B ได้ การสืบทอดคลาสแบบ Java ก็เพิ่มความซับซ้อนของตัวมันเองมากขึ้นเมื่อโปรแกรมค่อย ๆ วิวัฒน์ไปตามเวลา
  • Graydon ไม่ได้บอกว่า GC ทำให้การอนุมานเชิงเฉพาะที่อย่างเข้มแข็งเป็นไปไม่ได้ เขากำลังบอกว่าไม่ว่าด้วยเหตุผลใด นักออกแบบภาษาส่วนใหญ่เลือกทางที่สวนกับเป้าหมายนั้น และนั่นก็ดูจะจริงอย่างชัดเจน
    แน่นอนว่ามีตัวอย่างโต้แย้ง แต่ถ้ามองภาษาทั่วไปกระแสหลักแบบมี GC อย่าง Java, C#, Python ก็ถือว่าพูดได้ถูกต้อง เราอาจตีความได้ว่าแนวคิดดั้งเดิมของ object-oriented นั้นใกล้กับ actor model ในปัจจุบันมากกว่า และตั้งใจจะเปลี่ยนโครงสร้างข้อมูลที่มีเจ้าของผ่านการส่งข้อความเท่านั้น แต่การทำ object-oriented ในโลกจริงแทบไม่เคยเข้าใกล้เป้าหมายนั้น Java ไม่ได้ห้ามการเก็บ reference แบบเปลี่ยนแปลงได้ไปยัง object เดียวกันไว้ในหลาย object บทความนี้อธิบายประเด็นนั้นได้ดีกว่า: https://without.boats/blog/references-are-like-jumps/
  • คำถามสั้น ๆ: โค้ดนี้จะพิมพ์อะไรออกมา?
    void myMethod(final Map map) { map.remove("key"); int oldSize = map.size(); map.put("key", "val"); int newSize = map.size(); System.out.println(newSize - oldSize); }
    แก้ไข: ฉันอ่านปฏิเสธซ้อนผิดไป อ่านอีกรอบก็ยังงงอยู่ เขาหมายความว่าใน Java ต่างจาก JavaScript ตรงที่มีการอนุมานเชิงเฉพาะที่ใช่ไหม?

• ปกติผมชอบงานเขียนของ Graydon แต่บทความนี้ก็เหมือนบทความสาย formal methods หลายชิ้น ที่อาจทำให้ผู้อ่านซึ่งไม่รู้จักวงการนี้เข้าใจผิดได้ คล้ายกับการบอกว่าวิธีเปลี่ยนตะกั่วให้เป็นทองดีขึ้นในระดับเลขหลักเดียว แต่ไม่บอกว่ายังเหลืออีก 29 หลักกว่าจะไปถึงความคุ้มค่าเชิงปฏิบัติ
  ถ้าถามว่า การไม่มี alias ทำให้การตรวจพิสูจน์เชิงรูปแบบง่ายขึ้นมากไหม คำตอบคือใช่ แต่ถ้าถามว่ามันทำให้เราตรวจพิสูจน์โปรแกรมจริงได้อย่างใช้งานได้จริงและคุ้มต้นทุนไหม คำตอบคือไม่เลย ทุกวันนี้มีโปรแกรม วงจร และคอมโพเนนต์ที่ถูกตรวจพิสูจน์เชิงรูปแบบอยู่จริง แต่ถือเป็นข้อยกเว้น มีขนาดค่อนข้างเล็ก และถูกสร้างขึ้นด้วยวิธีที่ระมัดระวังเป็นพิเศษ คุณสมบัติที่ช่วยให้ทำ local reasoning ได้สำคัญก็จริง แต่ไม่ได้สร้างความเปลี่ยนแปลงอย่างมีนัยสำคัญต่อวิธีการที่รับประกันความถูกต้องของซอฟต์แวร์กระแสหลักได้อย่าง sound
  แม้แต่โปรแกรมในภาษาที่ไม่มีทั้ง heap, pointer, integer มีแค่ตัวแปร boolean และ loop ก็หมุนซ้ำได้ไม่เกินสองครั้ง ซึ่งยังห่างไกลจากความเป็น Turing-complete ก็ยังตรวจพิสูจน์เชิงปฏิบัติไม่ได้ เพราะมันลดรูปเป็น TQBF ได้ คุณอาจทำได้สำหรับคุณสมบัติบางอย่าง เช่น memory safety แต่ก็ยังไม่พอสำหรับสิ่งที่ซอฟต์แวร์ต้องการ ในช่วงปี 1970–90 เคยมีความหวังว่าถึงแม้ความซับซ้อนในกรณีเลวร้ายที่สุดจะจัดการยาก แต่การรับประกันเชิงเฉพาะที่และโครงสร้างของภาษาจะช่วยให้หลุดพ้นจากกรณีเลวร้ายที่สุดได้ แต่หลังจากนั้นก็พิสูจน์แล้วว่าไม่เป็นเช่นนั้น ความหวังที่ว่าซอฟต์แวร์ที่คนใช้งานจริงอยู่ไกลจากกรณีเลวร้ายที่สุดพอจนจะหา heuristic ที่ดีได้ ก็ดูจะไม่จริงอีกต่อไปแล้ว
  มีงานบรรยายที่พูดถึงเรื่องนี้: https://pron.github.io/posts/correctness-and-complexity
  ผลลัพธ์สำคัญคือคุณสมบัติที่น่าสนใจส่วนใหญ่ที่เราอยากตรวจพิสูจน์นั้น ไม่ compositional กล่าวคือ ต่อให้พิสูจน์คุณสมบัติของคอมโพเนนต์แต่ละตัว P1...Pn ได้แล้ว ต้นทุนในการพิสูจน์คุณสมบัตินั้นสำหรับ P1 ○ ... ○ Pn ก็ไม่ได้โตแบบ superpolynomial ตาม n เท่านั้น แต่ยังโตแบบ superpolynomial ตามขนาดของแต่ละคอมโพเนนต์ด้วย กล่าวคือยากพอ ๆ กับกรณีที่ไม่แยกส่วนเลย ความถูกต้องจึงไม่สามารถแยกย่อยได้ นี่จึงเป็นเหตุผลว่าทำไมทั้ง “เราตรวจพิสูจน์อะไรได้ค่อนข้างมาก” และ “สิ่งที่ตรวจพิสูจน์ได้เป็นเพียงหยดน้ำในมหาสมุทร” ถึงเป็นจริงพร้อมกัน และการถกเรื่อง formal methods ก็มักละช่องว่างนี้ไป

  • ตลอดกว่า 6 ปีที่ผ่านมา ผมพูดตรรกะเดิมนี้ซ้ำใน HN ไปหลายร้อยครั้ง และถึงจะได้รับคอมเมนต์ตอบกลับมากมาย ก็แทบไม่มีการเพิ่ม nuance อะไรเข้ามาเลย
    มันไม่ถึงกับผิดทั้งหมด แต่ก็ไม่ถูกทั้งหมดเช่นกัน หลายคนที่สนใจหัวข้อนี้มีโอกาสมากมายตลอดการถกเถียงซ้ำ ๆ หลายร้อยครั้งที่จะชี้ให้เห็นประเด็นนั้น แต่จุดยืนกลับไม่พัฒนาไปเลย น่าแปลกมาก ท่าทีแบบนี้ฟังดูปิดกั้นอย่างผิดปกติ และทำให้ทุกคนที่ร่วมบทสนทนาเสียเวลาเปล่า
  • ผมมองว่าการโฟกัสกับ soundness นั้น แทนที่จะช่วยเป้าหมายเรื่องซอฟต์แวร์ที่ถูกต้องมากขึ้น กลับดึงความสนใจออกจากเทคนิคที่ให้ผลลัพธ์ดีกว่าในทางปฏิบัติ มีเทคนิคเชิงปฏิบัติที่มีทฤษฎีรองรับ และบางครั้งก็ทำให้แม้แต่คนที่เคยคิดว่า soundness คือหนทางเดียวต้องประหลาดใจ: http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h...
    เรื่องแบบนี้เกิดซ้ำอยู่เรื่อย ๆ แม้ว่าวิธีแบบ sound จะมีการปรับปรุงสำคัญเกิดขึ้น แต่วิธีแบบ unsound ก็ยังสร้างความก้าวหน้าที่มากกว่ามากในงานจริง เพื่อมุ่งไปสู่ซอฟต์แวร์ที่ถูกต้องกว่า ตัวอย่างล่าสุดมากคือ https://antithesis.com แน่นอนว่าในบางสถานการณ์ เทคนิคแบบ sound อาจทรงพลังกว่าและใช้งานได้จริงกว่า จึงเป็นประเด็นที่ซับซ้อน
  • การที่เราน่าจะตรวจพิสูจน์ได้ว่าไลบรารี Rust ขนาดเล็กใช้ unsafe ได้ถูกต้องหรือไม่ เป็นความคาดหวังที่สมเหตุสมผล และแค่นั้นก็มีประโยชน์มากแล้ว

• ผมเพิ่งไปคอมเมนต์ที่เกี่ยวข้องไว้ในโพสต์ F* ด้วย ถ้ามองแค่ไวยากรณ์ โดยส่วนตัวผมชอบ F*/F# มากกว่า Rust แต่สำหรับซอฟต์แวร์ควบคุมการแสดงที่กำลังพัฒนาอยู่ ผมตัดสินใจใช้ Ada/SPARK2014
  ถ้า Rust อยากดึงดูดคนกลุ่มเดียวกับที่ Ada/SPARK2014 ดึงดูดได้ มันจำเป็นต้องมีมาตรฐานที่ตีพิมพ์อย่างเป็นทางการ แบบเดียวกับภาษาเก่าอย่าง C, Common Lisp, Prolog, Fortran และ COBOL ขณะนี้ Rust ก็กำลังเริ่มเข้าสู่พื้นที่นี้ เพราะ AdaCore กับ Ferrous Systems ร่วมมือกันเพื่อให้มีเครื่องมือตรวจพิสูจน์เชิงรูปแบบสำหรับ Rust แบบเดียวกับ Ada/SPARK2014 แต่ Rust ยังไม่มีมาตรฐานที่ตีพิมพ์ออกมา และมรดกของ Ada กับ SPARK2014 ก็ยิ่งใหญ่มาก

• น่าสนใจที่มันอาจมองได้ว่าเป็น GC แบบปรับแต่งและทำงานทันทีชนิดหนึ่ง ซึ่งทำงานได้เมื่อใช้ reference counting กับข้อมูลที่ไม่มีวงจรอย่างเคร่งครัด หรือเมื่อยอมรับการรั่วไหลจากวงจรได้ Python ใช้วิธีผสมระหว่าง reference counting + tracing collector ตามที่บทความอธิบายไว้ และเคยเห็นการดีพลอยในงานจริงที่บังคับให้ตัว tracing collector ทำงานเพียงหนึ่งครั้งต่อทุก ๆ คำขอ N ครั้ง
  Perl เป็น reference counting ล้วน แต่มี weak reference อยู่ จึงสามารถทำให้ข้อมูลเป็นแบบไม่มีวงจรในมุมมองของ reference counting ได้ โดยแลกกับการต้องใส่ใจว่าส่วนใดของโครงสร้างแบบวงจรที่ยังคงเก็บ reference เอาไว้ ส่วน Koka ในทางทฤษฎีใช้ reference counting แต่ในทางปฏิบัติพยายามดันให้มากที่สุดไปอยู่ในช่วง compile time และถ้ารับประกันได้ว่าใน y = x + 1 นั้น x มี reference เพียงตัวเดียวและจะไม่ถูกใช้อีก ก็สามารถนำพื้นที่เก็บข้อมูลเดิมกลับมาใช้กับ y เพื่อทำการเปลี่ยนแปลงแบบ in-place ได้
  Nim มี ORC ให้ใช้งาน ซึ่งคือการเพิ่ม implementation ของอัลกอริทึม Recycler ของ Bacon+Rajan เข้าไปบน automatic reference counting อัลกอริทึมนี้ถูกออกแบบมาให้เก็บเฉพาะวงจรในระบบที่อิงกับ reference counting จึงค่อนข้างเร็ว ถ้ากลับมาที่ฝั่ง Rust มี implementation ของ Recycler แบบ stop-the-world อยู่ที่นี่: https://github.com/fitzgen/bacon-rajan-cc และถูกเผยแพร่เป็น crate ชื่อ bacon-rajan-ccc ในฟอร์กนี้: https://github.com/mbartlett21/bacon-rajan-cc ส่วน Alternative ใน README มีลิงก์ไปยังการทดลองอื่น ๆ ในพื้นที่เดียวกัน ถ้าหาบทความวิชาการของ Recycler ได้ยาก ผมได้รวบรวมสำเนาไว้ใต้ https://trout.me.uk/gc/ และถ้าชอบแนวนี้ก็น่าจะสนุกกับบทความใต้ https://trout.me.uk/lisp/ ด้วย

  • Firefox ก็ใช้ทั้ง reference counting และ cycle collector ที่อิงกับ trial deletion เพื่อจัดการวงจรระหว่างอ็อบเจ็กต์ DOM ฝั่ง C++ กับ JS ด้วย อันที่จริง Graydon เป็นคนทำ implementation แรกเริ่ม
  • https://github.com/chc4/samsara ก็น่าดูเหมือนกัน เป็น implementation ของ concurrent GC algorithm แบบเดียวกันสำหรับ Rust ส่วน implementation ฝั่ง C++ อยู่ที่ https://github.com/pebal/sgcl

• ผมรู้สึกใจร้อนกับเรื่อง การตรวจพิสูจน์เชิงรูปนัยของโปรแกรม การพิสูจน์ว่าโปรแกรมทำตามสเปกอย่างถูกต้องนั้นน่าสนใจในทางทฤษฎี แต่มีประโยชน์เชิงปฏิบัติไม่มาก
  การเขียนสเปกที่ถูกต้องก็ยากพอ ๆ กับการเขียนโปรแกรมให้ถูกต้อง ดังนั้นปัญหาที่ยากไม่ได้ถูกแก้ แค่ถูกย้ายที่เท่านั้น แม้ว่าจะมีกรณีใช้งานเชิงปฏิบัติของวิธีเชิงรูปนัยอยู่บ้าง แต่พบไม่บ่อย

  • ถ้าเป็นสเปกที่สมบูรณ์ก็จริง แต่โดยทั่วไปนั่นไม่ใช่เป้าหมายจริง สิ่งที่มักอยากพิสูจน์คือคุณสมบัติสำคัญบางอย่าง เช่น ฟังก์ชันนี้จะจบการทำงานเสมอ หรือฟังก์ชันนั้นจะคืนค่าอาร์เรย์ที่เรียงลำดับแล้วเสมอ
    เมื่อทำแบบนั้นได้ ก็สามารถบังคับเป็น precondition ได้ เช่น ก่อนส่งอาร์เรย์เข้าไปยังฟังก์ชันหนึ่ง คุณต้องแสดงได้ก่อนว่าอาร์เรย์นั้นถูกเรียงลำดับไว้แล้ว

• เขียนเมื่อวันที่ 15 พฤษภาคม 2024 และวันนั้นคือ วันครบรอบ 9 ปีของ Rust 1.0

• ผมอ่านบทความของ Boats ที่ลิงก์ไว้แล้ว และมันยอดเยี่ยมมาก น่าทึ่งที่คำอ้างของ Hoare จากเมื่อ 50 ปีก่อนยังเกี่ยวข้องอยู่ และยังถ้อยคำดีมากด้วย

• คงจะดีถ้ามีอะไรอย่าง type guard ตอน compile time ที่เรียบง่ายกว่านี้ได้ เมื่อ trait bound เพิ่มพอกพูนขึ้น การอ่านโปรแกรมระดับ type ก็ยากขึ้น
  ตัวอย่างเช่น Where <<::Output as G>::Output as H>::Output: HList + Z หรือ type Output = <<::Output as G>::Output as H>::Output; ประมาณนี้ แล้วพอใส่ Cons>>> เข้าไป ก็เริ่มตระหนักว่าตัวเลขอย่าง U8 ของ TypeNum เองก็จริง ๆ แล้วเป็นการซ้อน Cons>> อยู่เหมือนกัน ในพื้นที่นี้สามารถสร้างความคืบหน้าและทำให้เกิดการตรวจพิสูจน์แบบที่ต้องการได้ แต่ข้อความ error อาจต่างจากวิธีที่นักพัฒนามนุษย์เขียนโค้ดมาก และตัว implementation เองก็ทรมานมาก
  สิ่งที่ทำให้ประสบการณ์นักพัฒนาดูน่าทึ่งคือ มันไม่ใช่ “แค่ฟังก์ชัน” แต่เป็นการผสมกันของ generic บางตัวกับ associated type ผมอยากใช้การตรวจแบบสไตล์รันไทม์ แต่ให้มันรันตอน compile time ทว่าเพื่อจะทำแบบนั้นได้ กลับต้องเขียนโค้ดที่ต่างออกไปมาก สุดท้ายแล้ว การทำให้ Rust ระดับ compile time แบบ type-level เรียบง่ายขึ้น เป็นเชิงฟังก์ชันมากขึ้น และอ่านง่ายขึ้น อาจเป็นทางที่จะทำให้โปรเจ็กต์วิเคราะห์เชิงรูปนัยแบบนี้มอบประสบการณ์ที่ดีทั้งต่อผู้ดูแลและผู้ใช้ สรุปคือผมอยากได้ comptime Rust และก็สงสัยเหมือนกันว่า Future ที่อิงกับ Pin<&mut Self> นั้นแข็งตัวไปแล้วหรือยัง ผมอยากลองทดลอง implementation ภายในของ async/await แบบอื่น ๆ แต่ไม่รู้จะเริ่มจากตรงไหน