สรุปบทความ Why Writing Correct Software Is Hard ของ pron.github.io เรื่อง halting problem ที่บอกว่าไม่มีอัลกอริทึมไหนตัดสินได้ว่าโปรแกรมจะจบหรือไม่จบ พร้อมตัวอย่างโค้ด 10 บรรทัดที่พิสูจน์ไม่ได้เพราะเท่ากับ Goldbach conjecture
มีบทความเก่าที่กลับมาติดเทรนด์อีกครั้งในเวลานี้ คือ Why Writing Correct Software Is Hard ของ Ron M"or (pron.github.io) เขียนครั้งแรกปี 2016 จาก talk ที่งาน Curry On
มันเป็นบทความที่อ่านแล้วรู้สึกว่า "เอ๊ะ ทำไมเรื่องนี้มันจริง" — เพราะมันไปได้ถึงระดับทฤษฎีบทพิสูจน์ไม่ได้ และมีตัวอย่างโค้ดจริงที่มนุษย์พยายามพิสูจน์มา 270 ปีแล้วยังไม่สำเร็จ
โจทย์ของบทความคือคำถามที่ดูเรียบง่ายมาก: ทำไมการเขียนโปรแกรมให้ถูกต้องถึงยาก?
คำตอบคือ: มันยาก เพราะมันต้องยาก ไม่ใช่เพราะเครื่องมือไม่ดีพอ บทความนี้รวมผลจากทฤษฎีการคำนวณ (computability theory) และทฤษฎีความซับซ้อน (complexity theory) มาชี้ให้เห็นว่าโปรแกรมกับ "ความเข้าใจอย่างครบถ้วน" ซึ่งเป็นสิ่งที่จำเป็นต่อการพิสูจน์ความถูกต้อง อยู่ในสถานะที่ขัดแย้งกันโดยธรรมชาติ
เรื่องราวเริ่มจาก David Hilbert ในปี 1900 ที่ตั้งโปรแกรมไว้สามข้อ:
ฮิลเบิร์ตเชื่อว่า "เราต้องรู้ แล้วเราจะรู้" และประโยคนี้ถูกสลักไว้บนหลุยสังขารของเขา
เส้นชีวิตของโปรแกรมนั้นจบในเวลาไม่กี่วัน:
พูดง่าย ๆ คือ: ไม่มีอัลกอริทึมใดที่บอกได้ว่าโปรแกรมที่กำหนดจะจบหรือไม่จบ เสมอ
หลักฐานเป็นการหักล้าง (diagonalization):
H(M, x) := IF M halts on x THEN TRUE ELSE FALSEสมมติว่ามีโปรแกรม H แบบนี้อยู่จริง เราสร้าง G:
G(y) := IF H(y, y) = FALSE THEN TRUE ELSE loop foreverแล้วเอา G ไปรันด้วย G เอง → ขัดแย้ง เพราะถ้า G บอกว่า H(G, G) เป็น FALSE แปลว่า G จะวนไม่จบ แต่ในกรณีนั้น H บอกว่า G จบ ซึ่งขัดกันเอง
ที่สวยงามคือ Halting Theorem ให้ corollary ที่ใกล้เคียงกับการเขียนโค้ดมากกว่าที่คิด เช่น Reachability: ไม่มีโปรแกรม R ที่รับโปรแกรม M, สถานะเริ่มต้น I แล้วบอกได้ว่า M จะไปถึงสถานะ S หรือเปล่า
และ Rice's Theorem: สำหรับ property ที่ไม่ trivial ใด ๆ ไม่มีอัลกอริทึมที่ตัดสินได้ว่าโปรแกรมคำนวณฟังก์ชันที่มี property นั้นหรือไม่ ตัวอย่างง่าย ๆ: ไม่มีอัลกอริทึมที่บอกได้ว่า output ของโปรแกรมเป็นกำลังสองของ input เสมอหรือไม่
ถ้าตัดสินใจไม่ได้ว่าโปรแกรมจะจบหรือไม่จบเมื่อไม่จำกัดเวลา ลองจำกัดเวลาดีกว่า: bounded halting — จะหยุดภายใน n ขั้นตอนไหม?
คำตอบคือ Θ(n) — เร็วกว่านั้นทำไม่ได้ คุณไม่มีทางรู้ว่าโปรแกรมจะทำอะไรได้เร็วกว่าการรันมัน เพราะการหักล้างแบบเดียวกันทำให้ขัดแย้ง
และผลที่ได้คือ Ω(|S|) โดย |S| คือจำนวน state ของโปรแกรม ซึ่งต่ำกว่านี้ทำไม่ได้ และผลนี้ยังแข็งแรงมาก แม้แต่ตัดความสามารถของเครื่องจักรลงจาก Turing-complete ให้เหลือแค่ FSM
นี่คือส่วนที่ผมชอบที่สุดของบทความ โค้ดชิ้นนี้ดูเรียบง่ายมาก — ทุก loop มี counter ที่ลดลง แปลว่ามัน "obviously terminates" ไม่มีเลขคณิตยาก ๆ มีแค่การลบ:
int foo(int x) {
if (x <= 2 || (x & 1) != 0)
return 0;
for (int i = x; i > 0; i--)
if (bar(i) && bar(x - i))
return i;
crash(); // reachable?
}
boolean bar(int x) {
for (int i = x - 1; i >= 2; i--)
for (int s = x; s >= 0; s -= i)
if (s == 0)
return false;
return true;
}แต่ประเด็นคือ foo จะ crash ก็ต่อเมื่อ Goldbach's conjecture เป็นเท็จ เพราะ bar เป็นการตรวจว่าเลขเป็น prime หรือไม่ (ถ้า ignore bug ใน implementation จริง ๆ)
และจุดที่ทำให้เรื่องนี้ไม่ใช่แค่ปัญหาเชิงทฤษฎี: ถ้าเราไม่รู้ว่าโค้ดนี้ผูกกับ Goldbach อยู่ หรือถ้า Goldbach ไม่เคยมีอยู่จริง เราจะยังรู้ได้อย่างไรว่ามันยากจะพิสูจน์แค่ไหน?
Yet mathematicians have failed to prove that this program never fails (i.e. reaches
crash()) for 270 years.
และบทเรียนที่หนักกว่านั้นคือ correctness ไม่ decompose — ต่อให้ bar ถูกต้องสนิท การประกอบเข้าด้วย foo ซึ่งเป็นแค่ loop ลดค่า + การเรียก + การ AND ง่าย ๆ ยังพิสูจน์ไม่ได้เลย
ถ้า modularization ช่วยได้จริง เราคงพิสูจน์โค้ดทั้งหมดได้ ซึ่งแปลว่าเราคงพิสูจน์ Goldbach ได้ด้วย
คำถามที่คนอ่านบทความนี้ต้องถามต่อแน่ ๆ: แล้ว types ล่ะ? ไม่มีคำตอบว่า types ช่วยพิสูจน์ความถูกต้องได้หรือเปล่า
คำตอบของบทความ: ช่วยได้ แต่ไม่ในแบบที่เราคิด
บทความตอบโจทย์ของ Rice's Theorem ก่อน เพราะดูเหมือนจะขัดแย้ง: ทำไมถึงเขียนโค้ด C, Java หรือ Haskell ให้คืนค่า int ได้ง่าย ๆ ถ้าเป็นเท็จตามทฤษฎี?
คำตอบคือ ความหมายของ "คืน int" จริง ๆ คือ "โปรแกรมไม่เคยจบ หรือโปรแกรมจบแล้วคืนค่าที่ตีความเป็นจำนวนเต็มได้" ซึ่งเป็น trivial property — ไม่มีข้อมูล bit ใด ๆ เลยเกี่ยวกับผลลัพธ์
แล้วก็มีข้อยกเว้นที่น่าสนใจ: ใน Haskell เราค่อนข้างง่ายที่จะพิสูจน์ว่า output เป็น string ของตัวเลข ซึ่งกำหนด bit ได้เยอะกว่า — แต่แล้วค่านั้นถูกสร้างโดย FSM ไม่ใช่ Turing machine จึงไม่ขัดกับ Rice's Theorem
สรุปคือ type system ที่ไม่มี dependent types คือ FSM property ประเภทหนึ่ง ซึ่ง model check ได้ ส่วนภาษาที่มี dependent types จำนวน concrete types จะเป็นอนันต์ → type inference จะ undecidable ไปด้วย
บทความยังให้แบบฝึกหัดที่ผมชอบ: ลองแทนทุก function body (รวม library functions) ด้วยฟังก์ชันที่ชัดเจนว่าเป็น FSM แล้วดูว่ามันยัง type-check ผ่านอยู่ไหม — ถ้าผ่าน แปลว่าคุณพิสูจน์แล้วว่า type system ของคุณไม่ได้ให้อะไรมากกว่า FSM (มีผู้ชี้ว่ากรณี polymorphic recursion ใน Haskell เป็น pushdown automaton แทน)
บทความนี้ไม่ได้บอกว่า "ทำอะไรไม่ได้เลย" แต่บอกว่าเราต้องจำกัดขอบเขตให้แคบลง
Model checkers — อัตโนมัติสำหรับ FSM ที่เล็ก ปัญหาคือ state explosion ที่โปรแกรม 30 บรรทัดก็มี state space ใหญ่มาก (ภาพของ alternating-bit protocol กับ CAN bus ช่วยให้เห็นภาพ)
Deductive proofs — พิสูจน์เป็นระบบ แม้แต่ logic ขั้นพื้นฐานที่สุด การพิสูจน์สั้น ๆ ที่มีอยู่สำหรับทุก tautology มีอยู่ก็ต่อเมื่อ NP = coNP ซึ่งเชื่อกันว่าไม่จริง (Cook-Reckhow)
Abstract interpretation — เทคนิคที่สวยงามและลึก ลดโปรแกรมเป็น abstraction ที่เล็กกว่า (แบบ parity ของ integer) แล้ว model check ที่นั่น ข้อเสียคือบางครั้งก็ตอบว่า "ไม่รู้"
Types — เป็น abstract interpretation อีกรูปแบบหนึ่ง ซึ่งอธิบายได้ว่าทำไมภาษาที่มี dependent types ถึง undecidable
บทความจบด้วยข้อเสนอให้ทำแบบ physics: embrace empiricism
เพราะโปรแกรมทั้งหมดที่เราสนใจถูกสร้างโดยมนุษย์ ถ้ามองมนุษย์เป็น TM ตัวใหญ่ตัวหนึ่ง เราอาจหา pattern ในเครื่องจักรที่มนุษย์สร้างเพื่อให้การพิสูจน์ที่พอจะทำได้ราคาไม่แพง แต่จะหา pattern ของมนุษย์เองไม่ได้ เพราะมันแพงกว่า ทางเดียวคือ ศึกษาเชิงประจักษ์ว่าคนจริง ๆ เขียนโค้ดยังไง
มีงานวิจัยของมหาวิทยาลัยโทรอนโตที่สนับสนุนแนวคิดนี้: พบว่า 92% ของ catastrophic failures ในระบบกระจายขนาดใหญ่เกิดจากการจัดการ non-fatal error ผิด และ 58% ของเคสสามารถตรวจจับได้ด้วยการเทสต์ error handling ง่าย ๆ ทีมวิจัยสร้าง linter ขึ้นมาตัวนึง แล้วมันจะป้องกัน catastrophic failure ได้ 33% ใน Cassandra, HBase, HDFS และ MapReduce
เรื่องนี้ชัดเจนว่าเป็นเรื่องจิตวิทยาของมนุษย์ ไม่ใช่เรื่องทฤษฎี
แล้วบทความก็ปิดท้ายด้วยคำของ Fred Brooks: "Complexity is the business we are in, and complexity is what limits us" — ถ้าคุณรู้สึกว่าความซับซ้อนเป็นแค่เรื่องของเครื่องมือที่ยังไม่ดีพอ ลองอ่านเรื่องนี้อีกที
เพราะมันเป็นบทความที่ตอบคำถามที่ทุกคนในวงการถามแต่ไม่กล้าหาคำตอบ: "ถ้าเรามี type system ดี ๆ, static analysis ดี ๆ, AI ช่วยเขียนโค้ดแล้ว เราจะได้โค้ดที่ถูกต้องไหม"
คำตอบคือ: ในระดับทั่วไป ไม่มี และจะไม่มี เพราะมันเป็นข้อจำกัดพื้นฐานของการคำนวณ ไม่ใช่ปัญหาทางวิศวกรรมที่จะหลุดรอดไปได้
แต่ข่าวดีคือมันไม่ได้แปลว่าเราต้องทำอะไรไม่ได้เลย — มันแปลว่าเราต้องเลือกว่าจะพิสูจน์อะไร ในขอบเขตไหน และยอมรับว่าส่วนที่เหลือต้องใช้ empiricism จัดการ
และบทความนี้ก็เป็นเหตุผลว่าทำไมผมถึงยังเขียนเทสต์อยู่ แม้จะมี AI ช่วยเขียนโค้ดให้
