Formal Methods: แค่แนวปฏิบัติทางวิศวกรรมที่ดีเท่านั้นหรือ? (2024)

 (brooker.co.za)
1 คะแนน โดย GN⁺ 2025-01-12 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • ในระบบขนาดใหญ่ ระบบแบบกระจาย และระบบระดับล่างที่มีความสำคัญสูง ควรมอง formal methods ไม่ใช่เป็น ขั้นตอนเสริมเพื่อความถูกต้องเท่านั้น แต่เป็นแนวปฏิบัติทางวิศวกรรมที่ช่วยลดเวลาและต้นทุน
  • ซอฟต์แวร์มีแนวโน้มที่การออกแบบและการนำไปใช้งานจะปะปนกันได้ง่าย การแก้แบบออกแบบในช่วงท้ายจึงนำไปสู่ การทำ implementation ใหม่ และต้นทุนจากการเปลี่ยน API ทันที
  • หากตรวจทานพฤติกรรมและอินเทอร์เฟซอย่างเป็นรูปธรรมก่อน implementation จะช่วยลดความหนาแน่นของบั๊กและปัญหาหลังขึ้น production และทำให้ไปถึงแบบออกแบบที่ถูกต้องได้เร็วขึ้น
  • ในพื้นที่ที่ความต้องการผู้ใช้เปลี่ยนเร็ว หรือ formalize ได้ยาก เช่น UI, เอกสาร และลอจิกราคา ประโยชน์ของการทำ formal design ล่วงหน้าแบบเต็มรูปแบบอาจลดลง
  • เครื่องมืออย่าง TLA+ และ P สามารถใช้ตรวจสอบการปรับแต่งและข้อจำกัดในขั้นออกแบบ เพื่อลด trade-off ระหว่างความถูกต้องกับประสิทธิภาพ ได้ด้วย

Formal methods ในฐานะแนวปฏิบัติทางวิศวกรรมที่ดี

  • Formal methods เป็นส่วนสำคัญของแนวปฏิบัติด้านวิศวกรรมซอฟต์แวร์ที่ดี
  • มีคุณค่าในการใช้งานเป็นพิเศษสำหรับวิศวกรที่ดูแล ระบบขนาดใหญ่, ระบบแบบกระจาย และระบบระดับล่างที่มีความสำคัญสูง
  • เริ่มจากสมมติฐานที่ว่า วิศวกรรมโดยแก่นแท้คือกิจกรรมเพื่อ ปรับเวลาและต้นทุนให้เหมาะสมที่สุด
    • โดยพิจารณาประสิทธิภาพ, ความสามารถในการขยาย, ความยั่งยืน และประสิทธิผลควบคู่กัน
  • Formal methods ไม่ได้ถูกหรือทำง่าย และไม่ได้เข้ากับวิธีพัฒนาทุกแบบเสมอไป แต่สัญชาตญาณที่ว่ามันมีแต่เพิ่มต้นทุนนั้นไม่ได้ถูกต้องเสมอ

สองเส้นทางในการลดต้นทุน

  • อย่างแรกคือ ลดการทำงานซ้ำ
    • ซอฟต์แวร์ต่างจากวิศวกรรมสาขาอื่นตรงที่การออกแบบและการสร้างมักเกิดขึ้นพร้อมกันได้ง่าย
    • สามารถเริ่ม implementation ได้แม้การออกแบบยังไม่คืบหน้าเพียงพอ
    • ความยืดหยุ่นนี้เป็นจุดแข็งของซอฟต์แวร์ แต่ก็อาจเปลี่ยนการวนซ้ำด้านการออกแบบให้กลายเป็นการวนซ้ำด้าน implementation และทำให้ต้นทุนสูงขึ้น
  • อย่างที่สองคือ จัดการต้นทุนของการเปลี่ยนแปลง
    • เมื่อ API หรือระบบมีลูกค้าแล้ว การเปลี่ยนแปลงจะยิ่งแพงและยากขึ้นมาก
    • ตาม Hyrum’s Law เมื่อมีผู้ใช้ API มากพอ ไม่ว่าสัญญาจะระบุไว้อย่างไร ก็จะมีใครบางคนพึ่งพาพฤติกรรมที่สังเกตได้ทุกอย่าง
  • การแยกพฤติกรรมของระบบผ่าน API เป็นแนวคิดสำคัญของวิศวกรรมซอฟต์แวร์ แต่ยังมีข้อจำกัดว่าผู้ใช้อาจพึ่งพารายละเอียด implementation ได้ถึงระดับหนึ่ง
  • แม้จะสามารถ reimplement ระบบที่อยู่หลัง API ได้ทั้งหมด แต่ abstraction ก็ไม่ได้ทำให้ต้นทุนการเปลี่ยนแปลงหายไปเอง
  • งาน formal design สามารถลดต้นทุนการทำงานซ้ำ และทำให้จัดการการเปลี่ยนอินเทอร์เฟซได้ตั้งแต่ช่วงที่เร็วขึ้น จึงเพิ่มความเร็วและประสิทธิผลในการสร้างซอฟต์แวร์

ระบบที่ formal design เหมาะสม

  • ไม่ได้ใช้กับซอฟต์แวร์ทุกชนิดในแบบเดียวกัน
  • สำหรับซอฟต์แวร์ที่วิวัฒน์เร็วหรือมีความต้องการผู้ใช้จำนวนมากซึ่ง formalize ได้ยาก คุณค่าของ การออกแบบล่วงหน้า อาจลดลง
    • UI, เว็บไซต์ และการทำลอจิกราคาอยู่ในกลุ่มนี้
    • ในพื้นที่เหล่านี้มักต้องทำงานซ้ำอย่างต่อเนื่อง ทำให้ต้นทุนของการออกแบบล่วงหน้าสูงขึ้นได้
  • แนวคิดพื้นฐานของ Agile คือการทำ implementation ควบคู่กับการเก็บ requirement เพื่อลดเวลาไปจนถึงการปล่อยใช้งาน
    • ทำให้ยังสามารถทำ implementation ให้เสร็จได้แม้การเก็บ requirement จะดำเนินต่อไป
    • ในหลายกรณี วิธีพัฒนาแบบขนานเช่นนี้เหมาะสมที่สุด หรือเป็นเงื่อนไขจำเป็นที่ทำให้เดินหน้าต่อได้
  • ในทางกลับกัน ส่วนใหญ่ของระบบขนาดใหญ่ แบบกระจาย และระดับล่าง มี requirement ที่เข้าใจกันดีแล้ว
    • อย่างน้อยก็มีส่วนของ requirement ที่ค่อนข้างคงที่และมีขนาดใหญ่พอ
    • ในกรณีนี้ formal design ล่วงหน้าสามารถลดการทำงานซ้ำและความหนาแน่นของบั๊กในขั้น implementation และหลังขึ้น production ได้อย่างมาก
  • ยิ่ง requirement ใกล้เคียงกับ กฎฟิสิกส์ มากเท่าไร คุณค่าของการออกแบบและ formal design ก็ยิ่งสูงขึ้น และยิ่งใกล้เคียงกับความคิดเห็นของผู้ใช้มากเท่าไร คุณค่านั้นก็ยิ่งลดลง

ข้อจำกัดของการจัดทำเอกสาร requirement และการ formalize

  • การเขียน requirement ของผู้ใช้ให้ชัดเจนมีคุณค่ามาก ไม่ว่าจะเป็นแบบ formal หรือไม่ formal
  • หากไม่เขียน requirement ก็จะเสียเวลา และผู้คนอาจเดินไปคนละทิศทางจนเกิดแรงเสียดทาน
  • การระบุ requirement ของมนุษย์ทั้งหมดในรูปแบบ formal อาจทำได้ยากหรือไม่คุ้มค่าในเชิงเศรษฐศาสตร์
    • requirement ด้านความงามของ UI
    • ความอ่านง่ายของเอกสาร
    • ความสอดคล้องของชื่อ API
  • ความเห็นที่แตกต่างเกี่ยวกับแนวทาง formal ยังมาจากความคิดที่ต่างกันว่าแนวทาง formal คืออะไร และมีคุณค่าในลักษณะใด
  • วิธีอย่าง UML ที่ย้ายโค้ดไปเป็นแผนภาพขนาดใหญ่ อาจมีคุณค่าต่ำลงหากไม่สามารถแตะคำถามยาก ๆ ได้โดยตรง
    • หากทำด้วยวิธีที่ไม่ดีหรือเครื่องมือที่ไม่ดี งานที่มีคุณค่าก็อาจกลายเป็นสิ่งไร้ประโยชน์ได้

Formal methods และเครื่องมือที่มีประโยชน์ในภาคปฏิบัติ

  • Formal methods และ automated reasoning เป็นสาขากว้าง และมีเครื่องมือหลากหลาย
  • ชุดเครื่องมือที่เคยมีประโยชน์ในระบบคลาวด์ขนาดใหญ่มีดังนี้
    • ภาษา specification อย่าง P, TLA+, Alloy และ model checker ที่เกี่ยวข้อง
    • เครื่องมือ simulation แบบ deterministic อย่าง turmoil
      • ใช้ร่วมกับ fuzzing เพื่อสำรวจ state space อย่างเป็นระบบผ่านการทดสอบ
    • ภาษาโปรแกรมที่เอื้อต่อการ verification อย่าง Dafny และ code verifier อย่าง Kani
    • เทคนิค numerical simulation
    • วิธีที่ใกล้เคียงกับ formal เช่น การวาด decision table, truth table และ explicit state machine บนไวต์บอร์ดหรือในเอกสารออกแบบ
  • Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 เป็นจุดเริ่มต้นสำหรับดู lightweight formal methods
  • การตรวจสอบ implementation ไม่ใช่เป้าหมายเดียว
    • เครื่องมืออย่าง TLA+ และ P มีคุณค่าสูงในการตรวจทานการออกแบบให้เร็วขึ้นและเป็นรูปธรรมมากขึ้นก่อนลงมือ implementation

สร้างซอฟต์แวร์ที่เร็วกว่าให้ได้เร็วขึ้น

  • ตอนเขียน How Amazon Web Services Uses Formal Methods ในปี 2015 จุดโฟกัสหลักคือความถูกต้อง
    • การตรวจสอบ safety และ liveness properties ของการออกแบบ
    • การไปถึงแบบออกแบบที่ถูกต้องให้เร็วขึ้น
  • ในกรณีของทีมที่ใช้ TLA+ กับระบบจัดการ lock ภายใน ประเด็นสำคัญคือการ “ตรวจสอบการปรับแต่งเชิงรุก”
  • เครื่องมืออย่าง TLA+ ไม่เพียงช่วยให้สร้างระบบได้เร็วขึ้น แต่ยังช่วยให้สร้างระบบที่เร็วขึ้นได้ด้วย
    • สำรวจ optimization ที่เป็นไปได้อย่างรวดเร็ว
    • ค้นหาข้อจำกัดที่สำคัญจริง ๆ
    • ยืนยันว่า optimization ที่เสนอถูกต้องหรือไม่
  • ในหลายกรณี formal methods ช่วยลด trade-off ที่ยากระหว่างความถูกต้องกับประสิทธิภาพ ซึ่งระบบมักตกลงไปได้ง่าย

คุณค่าของเครื่องมือที่ใช้ในขั้นออกแบบ

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

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

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

 
GN⁺ 2025-01-12
ความคิดเห็นบน Hacker News

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

    • ผมไม่ได้รู้สึกว่ามันเฉพาะทางถึงขนาดนั้น ต้นทุนที่ผู้คนพูดถึงลดลงมากในช่วงหลายทศวรรษที่ผ่านมา และผมเคยสอนเครื่องมืออย่าง TLA+ หรือ Alloy ให้กับนักพัฒนาได้ภายในไม่ถึงหนึ่งสัปดาห์
      ทุกวันนี้มันไม่ใช่ทักษะที่ต้องมีปริญญาเอกหรือการวิจัยหลายปีถึงจะเรียนรู้ได้อีกแล้ว และการเขียนสเปกระดับสูงพื้นฐานก็เช่นกัน เมื่อใช้ model checker คุณจะได้เรียนรู้อะไรบางอย่างเกี่ยวกับระบบที่กำลังสร้างโมเดล และแม้ใช้เพียงเพื่อทำเอกสารหรือฝึกอบรมก็ยังมีประโยชน์ พลังพื้นฐานของวิธีเชิงรูปนัยอยู่ที่การบังคับให้คิดให้สุดทาง นักพัฒนาหลายคนเชื่อว่าตนสามารถนำอัลกอริทึมแบบ concurrent ไปใช้งานได้ด้วยสมองของตัวเอง type checker และ unit test เล็กน้อยเท่านั้น แต่เมื่อรัน model checker แล้วพบข้อผิดพลาดในการออกแบบและสมมติฐาน ก็หลีกเลี่ยงไม่ได้ที่จะถ่อมตัวลง มีระบบแบบกระจายที่เล็กกว่าที่คิดอยู่มาก และ state space มักใหญ่กว่าที่คาดไว้มากก่อนจะลองทำให้เป็นรูปนัย
    • ไม่ใช่เรื่องว่าต้องทำทั้งหมดหรือไม่ทำเลย ผมทำงานกับ แบ็กเอนด์ที่เน้นผลิตภัณฑ์อย่างมากซึ่งไม่ได้ถูกระบุสเปกไว้อย่างสมบูรณ์ แต่บางส่วนของมันก็ถูกระบุสเปกเชิงรูปนัยไว้
      ตัวอย่างเช่น ผมใส่ property-based testing ให้กับ state machine ที่ยุ่งยากมาก เพื่อให้แน่ใจว่าไม่ว่าจะเรียก endpoint ด้วยอินพุตแปลก ๆ แบบใด state machine ภายในก็จะไม่ทำ transition ที่ไม่ถูกต้อง โค้ดรอบ ๆ ไม่มีสเปกเชิงรูปนัย แต่ state machine มี จึงทำเช่นนั้นได้ และยังพบ bug ละเอียดอ่อนที่ unit test แบบดั้งเดิมไม่มีทางจับได้ด้วย
    • “เชิงรูปนัย” หมายถึง “เขียนด้วยภาษาที่คอมพิวเตอร์ตีความได้” และนั่นก็คือสิ่งที่โปรแกรมเมอร์ทำ การเขียนโค้ดคือการเขียน ข้อกำหนดเชิงรูปนัยของพฤติกรรมโปรแกรม และตามนิยามแล้วซอฟต์แวร์ทั้งหมดต้องทำเช่นนั้น
      เพียงแต่หากต้องการได้ประโยชน์จากวิธีเชิงรูปนัย ก็ต้องเปรียบเทียบพฤติกรรมของโปรแกรมกับสิ่งอื่นที่ไม่ใช่ตัวโปรแกรมเอง และสิ่งอื่นนั้นก็ต้องเขียนด้วยภาษาเชิงรูปนัยด้วย ต้องเข้าใจพฤติกรรมที่ต้องการอย่างแม่นยำ แต่ไม่จำเป็นต้องครอบคลุมพฤติกรรมทั้งหมดของซอฟต์แวร์ การทดสอบหน่วยแบบอัตโนมัติก็เป็นข้อกำหนดเชิงรูปนัยเช่นกัน และการรันมันก็คือวิธีตรวจสอบเชิงรูปนัย เพียงแต่เป็นสเปกที่อ่อนกว่าและการตรวจสอบที่อ่อนกว่าวิธีเชิงรูปนัยที่พูดถึงกันทั่วไป ไม่ได้มีความแตกต่างเชิงคุณภาพที่ชัดเจนทั้งในเชิงแนวคิดหรือเชิงปฏิบัติ หากเป็นซอฟต์แวร์ที่ใช้การทดสอบได้ ก็มีโอกาสสูงที่จะใช้วิธีระบุสเปกเชิงรูปนัยที่สมบูรณ์ยิ่งขึ้นได้เช่นกัน และความคุ้มค่าต่อค่าใช้จ่ายจะเรียนรู้ได้จากการลองผิดลองถูก เหมือนกับการเรียนรู้เรื่องการทดสอบ
    • ไม่ว่าจะต้องการหรือไม่ requirements ก็จะเกิดขึ้นอยู่ดี ต่างกันแค่ว่าจะค้นพบในขั้น requirements engineering แล้วตรวจสอบด้วยเอกสารข้อความง่าย ๆ พร้อมจัดการความขัดแย้ง หรือจะรู้ตัวหลังจากเขียนโค้ดผิดไปแล้ว หรือให้ลูกค้าพบใน “sprint review”
      ท้ายที่สุดเป็นปัญหาว่าจะยอมใช้เงินและเวลาเพิ่มอีกเท่าใดเพื่อให้ถูกเรียกว่า “agile” ในทางย้อนแย้ง ขั้น requirements แบบดั้งเดิมกลับเป็นวิธีที่ถูกที่สุดในสามแบบ และยังสอดคล้องกับจิตวิญญาณ agile ดั้งเดิมมากที่สุด เพราะได้บรรจบกับลูกค้าอย่างรวดเร็วในจุดที่ต้นทุนการเปลี่ยนแปลงถูกที่สุด คือการแก้ข้อความหนึ่งบรรทัด
    • ประเด็นหลักดูเหมือนจะใกล้กับ ความสามารถในการทำให้เป็นรูปนัย มากกว่าการออกแบบล่วงหน้า ตัวอย่างเช่น ระบบอัตโนมัติสำหรับเคลมประกันมักไม่สามารถออกแบบได้ตั้งแต่ต้น เพราะการทำงานของบริษัทประกันหลายแห่งไม่ได้ถูกระบุไว้อย่างชัดเจน แต่สามารถปรับปรุงระบบอัตโนมัติไปพร้อมกับการได้รับข้อมูลจากการโต้ตอบได้
      ถึงอย่างนั้น ก็ยังได้ประโยชน์จากการตรวจสอบว่าไม่ได้พลาดทุกกรณีไปหรือไม่ และไม่มีความขัดแย้งภายในระบบหรือไม่

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

    • ผมคิดว่าเหตุผลที่ UML ไร้ประโยชน์คือ ไดอะแกรมเดียวกันแต่คนต่างกันเข้าใจต่างกัน และแม้มันจะซับซ้อนมาก ก็ยัง ตรวจสอบไม่ได้ จึงสร้างไดอะแกรม UML ที่ขัดแย้งในตัวเองหรือไม่สมเหตุสมผลได้
      เมื่อเจอปัญหาที่คิดยาก เราก็จะใช้ “วิธีการ” บางอย่าง ถ้าเป็นโปรโตคอลสื่อสาร การอธิบายด้วย state machine ก็เหมาะ และ TLA ก็เข้ากับช่องว่างนั้นได้ดีกว่า ช่วงหลัง ๆ ปัญหาที่คุ้มจะทุ่มแรงขนาดนั้นมีไม่มาก แต่ถ้ามีปัญหาแบบนั้นขึ้นมา มันก็มีคุณค่ามหาศาล ภาษาเฉพาะโดเมนก็เช่นกัน หากอยากหลีกเลี่ยงปัญหาหลายอย่าง การใช้ parser framework ย่อมดีกว่าการเขียน parser เองมาก ตอนนี้งานทำซ้ำส่วนใหญ่เกิดจากการเปลี่ยนข้อกำหนด และจากการที่ลูกค้าพูดว่า “ไม่ใช่อันนั้น” ทั้งที่ยังไม่รู้จริง ๆ ว่าต้องการอะไรจริง ๆ ส่วนหนึ่งเป็นเพราะคนที่ร้องขอไม่ได้คิดให้พอถึงนัยของความต้องการของตัวเอง แต่ที่ใหญ่กว่าคือความรู้ที่จำเป็นต่อการตัดสินใจที่ดีไม่ได้ถูกรวบรวมไว้ในที่เดียวอย่างเพียงพอ
    • ผมคิดว่าสาเหตุที่วิธีการเชิงรูปนัยไม่ได้ถูกใช้แพร่หลาย คือในความเป็นจริงมีขอบเขตธุรกิจไม่มากนักที่ต้องทุ่มเวลาและต้นทุนมากเพื่อยกระดับความถูกต้องของตรรกะโดเมนจาก 98% เป็น 99.99%
      วิธีการเชิงรูปนัยเป็นการลงทุนขนาดใหญ่อย่างชัดเจน อย่างไรก็ดี แม้มันจะไม่ได้กลายเป็นมาตรฐานทั่วไป แต่แนวคิดบางส่วนของมันก็ได้เข้าไปอยู่ใน type system สมัยใหม่แล้ว
    • ผมเคยสัมผัสการตรวจสอบเชิงรูปนัยเฉพาะในบริบทของวิชาฮาร์ดแวร์ มันคล้ายกับการเขียนโปรแกรม แต่ผลคุ้มค่าต่อค่าใช้จ่ายต่างกันโดยสิ้นเชิง ชิปกายภาพแก้ไขได้ยากหลังผลิต และรูปแบบการออกแบบก็ต่างกันมาก
      ความรู้สึกที่ได้รับคือ เพียงเพราะความเข้มงวดของตัวตรวจสอบเชิงรูปนัยต้องจบงานให้ได้ภายในเวลาและหน่วยความจำที่สมเหตุสมผล มันก็เท่ากับบังคับขีดจำกัดต่อความซับซ้อนของการออกแบบแล้ว บางทีชัยชนะที่แท้จริงของการบังคับใช้การตรวจสอบเชิงรูปนัย อาจอยู่ที่การแก้ปัญหา “ซอฟต์แวร์มีขนาดใหญ่ ซับซ้อน และทำให้ถูกต้องได้ยาก” ด้วยการทำให้การรับมือกับโปรแกรมขนาดใหญ่และซับซ้อนกลายเป็นเรื่องน่ารำคาญ
    • ถ้าจะต้มกบตัวนี้อย่างช้า ๆ ไม่ควรสอน TLA ตรง ๆ แต่ควร ขโมยภูมิปัญญา จากมันมาใช้ Type system ยืมหลายอย่างมาจาก Hindley-Milner และตัวมันเองก็เป็นการพิสูจน์บางส่วนเชิงรูปนัยอยู่แล้ว
      อยากเห็นทายาทของ property-based testing ที่ใช้เทคนิค SAT หรือ TLA เพื่อลดขอบเขต input space อย่างรวดเร็วและทำซ้ำได้ จากการ parsing และ code coverage มันควรอนุมานได้ว่า การส่งค่า 12 ให้ฟังก์ชันไม่สามารถไปยัง branch ที่ต่างจาก 11 ได้ แต่ค่าอย่าง -1 หรือ 2^17 < n < 2^32 อาจแตกต่างกันได้
    • ตรรกะที่ว่า “ถ้ามันมีประโยชน์จริง คนก็คงใช้กันมากกว่านี้” ไม่ใช่ตรรกะที่ดีในสาขาไหนเลย และใน การพัฒนาซอฟต์แวร์ ยิ่งแย่เป็นสองเท่า
      ทุกวันนี้โครงการซอฟต์แวร์ส่วนใหญ่ก็ยังล้มเหลวอยู่ นี่ไม่ใช่ “ความล้มเหลวของตลาด” แต่ใกล้เคียงกับ “ล้มเหลวในการสร้าง” ธรรมดามากกว่า

  • วิธีการเชิงรูปนัยแบ่งได้กว้าง ๆ เป็นสองสาย คือ วิธีการภายนอก ที่แยกจากตัวโค้ดเองและโดยปกติใช้อนุมานสเปกของโค้ด กับ วิธีการภายใน ที่เข้าไปอยู่ในโค้ดและอนุมานโค้ดโดยตรงมากขึ้น
    ในเชิงประวัติศาสตร์ วิธีการภายในอย่าง type system อนุมานโค้ดในระดับฟังก์ชัน ส่วนวิธีการภายนอกอย่าง model checker ที่ตัดสินได้ เช่น Spin/P จัดการกับโมเดลของโค้ดที่อธิบายด้วย formalism อย่าง automata ตอนนี้ผมมองว่าเป็นยุคทองของงานวิจัยวิธีการเชิงรูปนัย และดูเหมือนว่ากระแสเริ่มนิยมวิธีการภายนอกน้อยลงเรื่อย ๆ เมื่อเทียบกับวิธีการภายในที่ถูกผลักดันโดยพัฒนาการของ type system และโครงการอย่าง Verus https://github.com/verus-lang/verus

    • เครื่องมืออย่าง TLA+ ทำงานได้ดีเพราะมุ่งเป้าไปที่ ภาษา specification ที่เล็กมาก
      เคยเห็นคำถามว่าสิ่งนี้จะทำงานอย่างไรกับภาษาที่มี footprint ใหญ่อย่าง Rust แต่ยังไม่เห็นคำตอบที่ดี อยากอ่านเพิ่มเติม
    • ถ้าโครงการ Verus ที่ลิงก์ไว้ก็ให้เขียน specification ความถูกต้องโดยตรงเหมือนกัน ผมก็ไม่ค่อยเข้าใจว่าการแบ่งแบบนั้นมีความหมายอย่างไร
      ฟังดูเหมือนบอกว่าวิธีการภายในเป็นที่นิยมกว่าเพราะไม่ต้องเขียนและดูแล specification แยกต่างหาก แต่ในความเป็นจริงไม่ใช่อย่างนั้น

  • ส่วนที่พูดถึง วิธีการเชิงรูปนัยแบบเบา นั้นดี การดูแลชุดกลยุทธ์ proptest ไว้ข้าง ๆ codebase ไม่ได้เป็นการลงทุนที่มากกว่าการเขียน unit test ด้วยมือมากนัก แต่ให้ insight ที่ดีกว่ามาก เพราะมี coverage กว้างและ failure case ที่เล็กและเข้าใจได้
    เหนือสิ่งอื่นใด แนวทางนี้ยังเข้ากันได้ดีกับแนวปฏิบัติการพัฒนาซอฟต์แวร์ทั่วไปด้วย https://crates.io/crates/proptest

    • ช่วงนี้มีการสร้าง unit test ด้วย LLM กันมาก มันทำออกมาได้ค่อนข้างดี และสามารถสั่งให้ทำให้ละเอียดขึ้นอีกหน่อย หรือให้ทดสอบเงื่อนไขขอบเขตที่นึกออก หรือให้จัดการเงื่อนไขเฉพาะได้
      ผมพอรู้ว่าจะเขียน test ที่ดีอย่างไรและต้องใช้แรงแค่ไหน แต่ LLM สามารถสร้าง test ที่ดีกว่าได้เร็วกว่าผมมาก และเมื่อเป็นงานซ้ำ ๆ น่าเบื่อ มันอาจมีแนวโน้มที่จะไม่ทำแบบลวก ๆ มากกว่าผมที่ความอดทนลดลงเสียอีก ถ้าเป็นวิศวกรซอฟต์แวร์ ก็ควรมีปฏิกิริยาอัตโนมัติที่จะทำให้งานที่รู้สึกว่าซ้ำ ๆ เป็นระบบอัตโนมัติ และทุกวันนี้เอกสารก็ถูกสร้างขึ้นได้ จึงทำบ่อยขึ้นและเร็วขึ้นด้วย LLM อาจก่อให้เกิดการปฏิวัติเล็ก ๆ ในการนำการตรวจสอบเชิงรูปนัยมาใช้ การสร้าง specification ที่ถูกต้องนั้นน่าเบื่อ แต่ถ้ามีบริบทเพียงพออย่างโค้ดที่ทำงานได้ เอกสาร และ hint ต่าง ๆ ก็อาจเป็นงานที่ค่อนข้างง่ายสำหรับ LLM ถ้าสามารถให้มันสร้างขึ้นมาแล้วเราค่อยไล่อ่าน แทนที่จะต้องเขียน specification ทั้งหมดเอง ก็จะทำให้อยากทำมากขึ้นมาก การใช้ Rust เองก็เป็นสัญญาณว่าให้ความสำคัญกับความถูกต้อง และ compiler ของมันก็ใกล้เคียงกับเครื่องมือที่พิสูจน์ได้มากที่สุดว่าระบบน่าจะถูกต้องโดยไม่ต้องใช้วิธีการเชิงรูปนัย จึงมีโอกาสง่ายกว่ามากเมื่อเทียบกับการเอาวิธีการเชิงรูปนัยไปเสริมให้ภาษาที่ไม่มีทั้ง compiler หรือ explicit type
    • proptest หรือ qcheck ไม่ใช่วิธีการเชิงรูปนัย แต่เป็น การทดสอบแบบสุ่ม

  • การตรวจสอบความถูกต้องเชิงรูปแบบของซอฟต์แวร์ยังยากเกินกว่าจะคุ้มค่าในการใช้งาน เว้นแต่เป็นกรณีสุดโต่ง ในทางกลับกัน การตรวจสอบความถูกต้องเชิงรูปแบบของฮาร์ดแวร์ อยู่ในระดับที่ไม่มีเหตุผลจะไม่ใช้
    พยายามเรียนรู้อยู่เรื่อย ๆ แต่สำหรับระบบส่วนใหญ่ ต้องเป็นผู้เชี่ยวชาญระดับ “คนที่เขียนคอมไพเลอร์เอง” ตัวอย่างเช่น เคยพยายามพิสูจน์ encoder/decoder แบบ varint ซึ่งทำได้สำหรับ 1–2 ไบต์ แต่เกินกว่านั้นทำไม่ได้ พอขอความช่วยเหลือ ก็พบว่าเป็นเพราะรายละเอียดภายในที่ไม่มีทางรู้ได้ เช่น คอมไพเลอร์ภายในคลี่ลูปแค่ 5 ครั้ง ช่วงนี้กำลังเรียน Lean อยู่ และก็ชอบนะ แต่ดันเจอเอกสารทำนองนี้: “Definitional equality includes η-equivalence…” ไม่ได้ตั้งใจจะด้อยค่า Lean ตรงกันข้าม มันดูเหมือนเป็นหนึ่งในตัวเลือกที่มีเอกสารดีกว่าด้วยซ้ำ

    • อยากรู้ว่าเคยลอง FizzBee.io ไหม มันใช้ ไวยากรณ์คล้าย Python และตัวอย่างก็น่าดู: https://fizzbee.io/examples/two_phase_commit_actors/#complet...
      เทคนิคเชิงรูปแบบไม่จำเป็นต้องซับซ้อนเสมอไป ปัญหาคือเทคนิคเชิงรูปแบบส่วนใหญ่ถูกออกแบบมาเหมือนแบบฝึกหัดเชิงวิชาการเพื่อแสดงหัวข้อเฉพาะที่ศาสตราจารย์สนใจ TLA+ ก็ใกล้เคียงกับการถูกออกแบบมาเพื่อเขียน论文มากกว่า
    • อาจดูน่ากลัว แต่แนวคิดเหล่านั้นจริง ๆ แล้วล้วนเรียบง่ายมาก และมีโอกาสสูงว่าเป็นสิ่งที่คุณคุ้นเคยอยู่แล้ว

  • ในบรรดาเทคนิคเชิงรูปแบบแบบเบา ๆ สิ่งที่ไม่ค่อยเป็นที่รู้จักแต่ผมชอบคือการตรวจสอบ trace โดยใช้ linear temporal logic: https://en.m.wikipedia.org/wiki/Linear_temporal_logic
    โดยพื้นฐานแล้วแค่ต้อง log event และในสถาปัตยกรรมแบบ event-driven ก็แทบได้มาฟรีอยู่แล้ว จากนั้นก็รัน predicate อย่าง Always(Locked, Implies(Eventually(Unlocked))) บน execution trace ได้เลย ใช้กับ trace ในอดีตก็ได้ และผสานกับ stress test หรือ fuzzing เพื่อสำรวจ state space ได้ด้วย เรียบง่าย ทรงพลัง ใช้ได้กว้าง และไม่ต้องมีโมเดล แค่มี predicate ก็พอ

    • เป็นการแยกแยะเล็กน้อย แต่นี่ใกล้เคียงกับ การทดสอบ มากกว่า เพราะตรวจสอบสูตรกับเพียงบางชุดย่อยของ trace ของระบบ
      เทคนิคเชิงรูปแบบสื่อถึงหลักฐานที่ครอบคลุมเกี่ยวกับพฤติกรรมของระบบ ใน TLA หรือระบบคล้ายกัน แม้จะเป็น state machine ไม่ใช่ระบบจริง แต่ผลลัพธ์คือการพิสูจน์ว่า property แบบ LTL/CTL/TLA เป็นจริงสำหรับพฤติกรรมทั้งหมดของระบบ นั่นคือ trace หรือ trace tree

  • การอภิปรายก่อนหน้านี้เกิดขึ้นเมื่อเดือนมิถุนายน 2024: https://news.ycombinator.com/item?id=40753989

    • เมื่อกางออก จะเป็นสองบทความต่อไปนี้: Formal methods: Just good engineering practice? - https://news.ycombinator.com/item?id=40753989 - มิถุนายน 2024, 149 ความคิดเห็น
      15 Years of Formal Methods at AWS: Just Good Engineering Practice? - https://news.ycombinator.com/item?id=40283052 - พฤษภาคม 2024, 1 ความคิดเห็น

  • ช้าเกินไป แผนก็คือ การกลายเป็นฟอสซิล ในเร็ว ๆ นี้ และเอกสารใด ๆ ก็อาจถูกใช้เป็นหลักฐานที่เป็นโทษในศาลแห่ง Agile ได้

    • พูดแบบชวนถกเถียง ถ้ามีการค้นพบ “Agile ของแท้” ขึ้นมา เทคนิคเชิงรูปแบบ ก็คงเป็นสิ่งตรงข้ามโดยสิ้นเชิง เพราะสิ่งที่พิสูจน์ได้และทำซ้ำได้ถือเป็นการลบหลู่สำหรับผู้ศรัทธาแท้

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

    • แล้ว https://en.wikipedia.org/wiki/SPARK_(programming_language) ล่ะ
    • ถ้า “สร้างโค้ดคุณภาพสูงที่ไม่มีทางเบี่ยงเบนจากสเปก” ได้ก็คงมีประโยชน์ แต่มีปัญหาพื้นฐานอยู่ โค้ดนั้นเป็นรูปธรรมเกินไป
      ในสเปกเชิงรูปแบบ ปกติไม่ได้กำหนดรายละเอียดถึงระดับนั้น แต่กำหนดพฤติกรรมทั่วไปของระบบ ดังนั้นสเปกหนึ่งชุดมักสอดคล้องกับโปรแกรมจำนวนมากที่แตกต่างกันเล็กน้อย นี่ก็เป็นเหตุผลที่โค้ดไม่เพียงพอในฐานะเอกสาร เพราะเราไม่อาจรู้ได้ว่าอะไรคือการเลือกโดยตั้งใจ และอะไรคือการเลือกโดยบังเอิญ โค้ดเป็นรูปธรรมเกินไปสำหรับการอธิบาย requirement ระดับสูง ในทางกลับกัน การตรวจสอบโปรแกรมเทียบกับสเปกน่าจะมีโอกาสนำไปใช้ได้มากกว่า

  • ผู้สนับสนุนเทคนิคเชิงรูปแบบบางคนในปัจจุบันมองคนที่ไม่ใช้เทคนิคเชิงรูปแบบว่า “ขี้เกียจ” หรือ “โง่” และพยายามอ้างความเหนือกว่าเพราะตัวเอง “ทำสิ่งที่ถูกต้อง” หรือ “เชี่ยวชาญภาษาที่ซับซ้อน”
    แน่นอนว่าไม่ใช่ทั้งหมด และผมก็รู้จักคนดี ๆ อยู่ แต่บางคนจริง ๆ แล้วใกล้เคียงกับ คนที่ถนัดอยู่แค่อย่างเดียว มากกว่า ถ้าถามว่าในช่วงไม่กี่ปีที่ผ่านมาได้เรียนรู้หรือลองระบบเทคนิคเชิงรูปแบบอื่นอะไรบ้าง ก็มักตอบว่า “ยุ่งเกินไป” จนเรียนของใหม่ไม่ได้ เทคนิคเชิงรูปแบบที่ใช้ง่ายขึ้นในช่วงหลังมี FizzBee ซึ่งใช้ dialect ของ Python จึงอ่านเหมือน pseudocode, Quint ที่มีไวยากรณ์ง่ายกว่า และ P ที่มีไวยากรณ์คุ้นเคยสำหรับผู้ใช้ C# ผู้เขียนบทความนี้เองก็เคยเขียนว่าเทคนิคเชิงรูปแบบแก้ปัญหาของเขาได้เพียงครึ่งเดียว: https://brooker.co.za/blog/2022/06/02/formal.html
    แต่ปัญหาที่พูดถึงในนั้น PRISM ซึ่งไม่ใช่ของใหม่ก็แก้ได้อยู่แล้ว เพียงแต่ Brooker ไม่ยอมมองหาหรือเรียนรู้รอบ ๆ ตัวเท่านั้น