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

 (graydon2.dreamwidth.org)
1 คะแนน โดย GN⁺ 2024-05-17 | 1 ความคิดเห็น | แชร์ทาง WhatsApp

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

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

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

 
GN⁺ 2024-05-17
ความคิดเห็นจาก Hacker News

สรุปรวมความคิดเห็นจาก Hacker News

  • Rust และวิธีการเชิงรูปนัย

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

  • การอ้างอิงบทความของ Hoare ปี 1973

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

  • คำวิจารณ์ต่อการวิเคราะห์โปรแกรม

    • บทความนี้มองข้ามทั้งสาขาของการวิเคราะห์โปรแกรมไป
    • ภาษาอย่าง Java มี GC แต่ขาดการรองรับการให้เหตุผลเชิงท้องถิ่นที่แข็งแกร่ง
    • การวิเคราะห์ pointer และ escape analysis สามารถอนุมานความเป็นเอกเทศและตัดสินได้ว่า reference นั้นแยกจากกันหรือไม่

  • ความสงสัยต่อการพิสูจน์ความถูกต้องเชิงรูปนัย

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

  • F และ Ada/SPARK2014*

    • ชอบไวยากรณ์ของ F* มากกว่า แต่ใช้ Ada/SPARK2014 สำหรับระบบควบคุมที่เกี่ยวข้องกับความปลอดภัย
    • Rust ยังไม่มีมาตรฐานอย่างเป็นทางการ จึงดึงดูดผู้ใช้กลุ่มเดียวกับ Ada/SPARK2014 ได้ยาก

  • ข้อจำกัดของวิธีการเชิงรูปนัย

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

  • reference counting และ garbage collection

    • Python ใช้ hybrid ของ reference counting และ tracing
    • Perl ใช้ reference counting แบบล้วน แต่จัดการโครงสร้างแบบวนรอบด้วย weak reference
    • Nim ใช้ ORC เพื่อให้ระบบที่รวดเร็วซึ่งเก็บเฉพาะโครงสร้างแบบวนรอบ

  • ครบรอบ 9 ปีของ Rust

    • ร่วมฉลองครบรอบ 9 ปีของ Rust 1.0

  • แพตเทิร์น Typestate

    • ชอบอ่านบทความเกี่ยวกับแพตเทิร์น Typestate

  • type guard ตอนคอมไพล์

    • อยากให้สามารถเขียน type guard ตอนคอมไพล์ได้ง่ายกว่านี้
    • ข้อความ error ของโปรแกรมระดับ type มีความซับซ้อนและบั่นทอนประสบการณ์ของนักพัฒนา
    • จำเป็นต้องทำให้ความสามารถตอนคอมไพล์ของ Rust เรียบง่ายและเป็นเชิงฟังก์ชันมากขึ้น

สรุปนี้นำเสนอมุมมองที่หลากหลาย และเรียบเรียงให้วิศวกรซอฟต์แวร์ระดับเริ่มต้นเข้าใจได้ง่าย