วิธีเป็นโปรแกรมเมอร์ที่ดีขึ้นด้วยการทำข้อพิสูจน์เล็ก ๆ ในหัว

 (the-nerve-blog.ghost.io)
1 คะแนน โดย GN⁺ 2025-07-16 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • หากอยากเป็นโปรแกรมเมอร์ที่เก่งขึ้น สิ่งสำคัญคือการสร้าง นิสัยทำข้อพิสูจน์เล็ก ๆ ในหัวขณะเขียนโค้ด
  • แนวคิดอย่าง monotonicity, immutability, pre- และ post-conditions รวมถึง invariants เป็นแกนสำคัญของการทำมินิพรูฟลักษณะนี้
  • การออกแบบโดยคำนึงถึงขอบเขตผลกระทบของการเปลี่ยนโค้ดต่อทั้งระบบ (isolation, firewall) ช่วยลดความซับซ้อนและความเสี่ยงได้มาก
  • การใช้ induction ช่วยพิสูจน์ความถูกต้องของฟังก์ชันหรือโครงสร้างแบบเวียนเกิดได้เป็นลำดับขั้น
  • วิธีคิดแบบนี้พัฒนาได้จากการฝึกฝนและทำจนเป็นนิสัย และการฝึกพิสูจน์ทางคณิตศาสตร์รวมถึงการแก้โจทย์อัลกอริทึมช่วยได้มาก

บทนำและแนวคิดหลัก

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

Monotonicity

  • Monotonicity คือคุณสมบัติที่ฟังก์ชันหรือโค้ดดำเนินไปได้ในทิศทางเดียวเท่านั้น
  • ตัวอย่างหนึ่งคือการทำ checkpointing ซึ่งขั้นตอนของงานจะเดินหน้าอย่างเดียว และจะไม่ย้อนกลับไปรันงานที่ทำเสร็จแล้วอีก
  • ในตัวอย่างการเปรียบเทียบ LSM tree กับ B-tree นั้น LSM tree มีลักษณะที่พื้นที่ส่วนใหญ่สะสมเพิ่มขึ้น และจะลดลงเฉพาะในกระบวนการ compaction
  • เมื่อรับประกัน monotonicity ได้ เราจะตัดความเป็นไปได้ของบางสถานะหรือผลลัพธ์ที่ซับซ้อนออกไปได้อย่างเป็นธรรมชาติ หรือคาดการณ์ได้ง่ายขึ้น
  • Immutability ก็เป็นแนวคิดคล้ายกัน เพราะเมื่อค่าถูกกำหนดแล้วจะไม่เปลี่ยนอีก ทำให้ตัดความเป็นไปได้ของการเปลี่ยนสถานะออกไปได้

เงื่อนไขก่อนและเงื่อนไขหลัง (Pre- and post-conditions)

  • Pre-condition และ post-condition คือข้ออ้างที่ต้องเป็นจริงก่อนและหลังการทำงานของฟังก์ชัน
  • การติดตามเงื่อนไขเหล่านี้อย่างชัดเจนระหว่างเขียนฟังก์ชันช่วยทั้งด้านการคิดเชิงตรรกะและการทดสอบ
  • หากกำหนด post-condition ได้ชัดเจน ก็จะอนุมาน test case ระดับ unit test ได้ง่ายขึ้น
  • การเพิ่ม assertion เพื่อตรวจสอบเงื่อนไขเหล่านี้ในโค้ดและหยุดการทำงานตั้งแต่เนิ่น ๆ เมื่อเกิดสถานการณ์ไม่คาดคิด จะช่วยเพิ่มความคาดเดาได้และความปลอดภัย
  • บางครั้งฟังก์ชันอาจกำหนด pre-/post-condition ที่ชัดเจนได้ยาก แต่การค้นพบจุดนี้เองก็มีนัยสำคัญ

Invariants

  • Invariant คือคุณสมบัติที่ต้องเป็นจริงเสมอไม่ว่าในสถานการณ์ใด ทั้งก่อน ระหว่าง และหลังการทำงานของโค้ด
  • ตัวอย่างคลาสสิกของ invariant คือ สมการทางบัญชี ในระบบบัญชีแบบ double-entry (ยอดเครดิตรวม = ยอดเดบิตรวม)
  • หากแยกโค้ดทั้งชุดออกเป็นขั้นเล็ก ๆ แล้วพิสูจน์ว่าแต่ละขั้นยังคงรักษา invariant ไว้ได้ ก็จะช่วยรับประกันความสมบูรณ์ของระบบโดยรวม
  • มีวิธีใช้ listener หรือ lifecycle method เพื่อรักษา invariant เช่น constructor/destructor ของ C++ หรือ useEffect ของ React
  • เมื่อจุดที่เปลี่ยนมีน้อย หรือเส้นทางการทำงานไม่ซับซ้อน การตรวจสอบ invariant จะง่ายกว่ามาก

Isolation

  • หัวใจข้อหนึ่งของซอฟต์แวร์ที่ดีคือการเพิ่มหรือแก้ฟีเจอร์ใหม่โดยไม่ทำให้ระบบเดิมไม่เสถียร
  • เราควรเข้าใจ ‘รัศมีผลกระทบ’ (blast radius) ของการเปลี่ยนโค้ด และสร้าง ‘firewall’ เชิงโครงสร้างเพื่อลดขอบเขตการแพร่ของผลกระทบให้มากที่สุด
  • ในตัวอย่างของบริการ Nerve ผู้เขียนอธิบายแนวทางการออกแบบให้เส้นแบ่งระหว่าง query planner กับ query executor ชัดเจน และทำให้ส่วนที่แก้ไขไม่ล้ำผ่านเส้นแบ่งนี้
  • หากป้องกันไม่ให้การเปลี่ยนแปลงแพร่กระจายโดยไม่จำเป็น การตรวจสอบและการบำรุงรักษาจะง่ายขึ้น และความเสถียรก็จะสูงขึ้น
  • สิ่งนี้สอดคล้องกับปรัชญาของ OCP (Open-Closed Principle) ด้วย คือการขยายความสามารถโดยไม่เปลี่ยนพฤติกรรมเดิม

Induction

  • โปรแกรมจำนวนมากมีทั้ง ฟังก์ชันแบบเวียนเกิด หรือ โครงสร้างแบบเวียนเกิด และ induction เป็นเครื่องมือทรงพลังในการตั้งหลักเหตุผลกับสิ่งเหล่านี้
  • หากต้องการพิสูจน์การทำงานและความถูกต้องของฟังก์ชันเวียนเกิดอย่างเป็นขั้นตอน ต้องตรวจสอบทั้ง base case และ inductive step
  • ผู้เขียนยกตัวอย่างกระบวนการลดรูปโหนดในโครงสร้าง AST (syntax tree) และใช้การให้เหตุผลแบบอุปนัยในแต่ละขั้นเพื่อพิสูจน์การคงอยู่ของ invariant และความถูกต้องของการทำงาน
  • เมื่อซึมซับวิธีคิดแบบ induction ได้แล้ว การเขียนและตรวจสอบโค้ดแบบเวียนเกิดจะเป็นธรรมชาติและง่ายขึ้นมาก
  • นอกจากนี้ยังชวนให้ลองเปรียบเทียบกับความพยายามตรวจสอบแบบมองทั้งระบบ (holistic) ที่ไม่ใช่ induction ว่าวิธีไหนเป็นธรรมชาติกว่ากัน

Proof-affinity ในฐานะตัวชี้วัดคุณภาพ

  • ผู้เขียนเสนอว่าคุณลักษณะของโค้ดที่ดีคือ โค้ดที่เราสามารถวาดข้อพิสูจน์เล็ก ๆ ในหัวได้
  • หากโค้ดมีโครงสร้างอย่าง monotonicity, immutability, เงื่อนไขที่ชัดเจน, การแยก invariant, ขอบเขตแบบ firewall และการใช้ induction ก็จะพิสูจน์ได้ง่ายขึ้น และนั่นหมายถึงตัวโค้ดเองก็มีคุณภาพสูงขึ้นด้วย
  • หากโค้ดเข้าใจยากและตรวจสอบได้ลำบาก ก็เป็นสัญญาณว่าอาจต้อง refactor หรือทบทวนโครงสร้างใหม่
  • ในบริบทนี้ผู้เขียนเสนอให้ใช้คำว่า proof-affinity แทนคำว่า ‘พิสูจน์ได้’ ตรง ๆ
  • แม้ proof-affinity จะไม่ใช่องค์ประกอบเดียวของคุณภาพซอฟต์แวร์ แต่เป็นตัวเร่งสำคัญอย่างมากต่อการทำความเข้าใจ ขยาย ทดสอบ และดูแลรักษาโค้ด

วิธีพัฒนาทักษะ

  • วิธีคิดเชิงตรรกะแบบนี้ต้องอาศัยการฝึกฝนสะสมจนสามารถนำไปใช้ได้อย่างเป็นธรรมชาติในระดับไร้สำนึก
  • การเขียนข้อพิสูจน์ทางคณิตศาสตร์บ่อย ๆ และฝึกความสามารถในการให้เหตุผลเชิงตรรกะเป็นสิ่งจำเป็น
  • การแก้โจทย์อัลกอริทึม (เช่นคอร์ส EdX ของ Stanford, Leetcode ฯลฯ) ก็เป็นสนามฝึกที่ดี โดยเฉพาะถ้าเน้นโจทย์ที่ต้องอาศัยการลงมือทำอย่างรอบคอบและการคิดแบบพิสูจน์ ไม่ใช่แค่โจทย์แนวทริก
  • แทนที่จะค่อย ๆ แก้ผลลัพธ์หลายรอบจนถูก ควรฝึกให้เข้าใกล้คำตอบที่ถูกต้องตั้งแต่ครั้งแรก
  • เมื่อสร้างนิสัยนี้ได้แล้ว ความสามารถในการออกแบบระบบเชิงตรรกะและคุณภาพของโค้ดจะดีขึ้นอย่างมาก

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

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

 
GN⁺ 2025-07-16
ความคิดเห็นจาก Hacker News

  • มีตัวอย่างที่ตรงกับประเด็นนี้มาก เป็นตัวอย่างที่เรียบง่ายแต่ชวนทึ่ง นั่นคือ binary search นี่เอง แม้จะมีทั้งแบบแปรผันซ้ายและขวา แต่ถ้าไม่คิดเรื่อง loop invariant ก็ยากมากที่จะเขียนให้ถูกต้อง บทความนี้ อธิบายแนวทางแบบ invariant และยกตัวอย่างโค้ด Python ที่สอดคล้องกันไว้ ผู้เขียน Programming Pearls อย่าง Jon Bentley เคยให้โปรแกรมเมอร์ IBM ลองเขียน binary search แบบธรรมดา ปรากฏว่า 90% มีบั๊ก ส่วนใหญ่เป็นการพลาดจนเกิดลูปไม่รู้จบ สมัยนั้นยังต้องป้องกัน integer overflow กันเองด้วย จึงพอเข้าใจได้ระดับหนึ่ง แต่ถึงอย่างนั้นก็ยังเป็นสัดส่วนที่น่าตกใจอยู่ดี

    • พอเห็นแบบนี้ก็เลยเริ่มใช้ binary search เป็นคำถามสัมภาษณ์ ผู้สมัครที่มีชื่อเสียงดีประมาณ 2 ใน 3 เขียน implementation ที่ทำงานถูกต้องภายใน 20 นาทีไม่ได้ โดยเฉพาะกรณีง่าย ๆ ที่มักติดลูปไม่รู้จบ คนที่ทำสำเร็จมักเขียนได้เร็ว หนึ่งในสาเหตุคือหลายคนเรียนมาด้วย interface ที่ไม่เหมาะ Wikipedia ก็อธิบายว่า “กำหนดค่าเริ่มต้น L เป็น 0 และ R เป็น n-1” ซึ่งเป็นช่วงที่รวม R อยู่ด้วย แต่ในความเป็นจริง สำหรับอัลกอริทึมสตริงส่วนใหญ่ รูปแบบที่ไม่รวมขอบบน หรือก็คือ R เป็น n มักดีกว่า อยากลองทดสอบสมมติฐานนี้จริง ๆ โดยให้คนจำนวนมากเขียนด้วย function prototype และค่าเริ่มต้นที่ต่างกัน แล้วเทียบกันว่าแบบ inclusive upper bound, exclusive upper bound และแบบ length ทำให้เกิดบั๊กมากน้อยแค่ไหน

    • อันที่จริง binary search เป็นตัวอย่างคลาสสิกที่การจัดการ index ยุ่งยากแทบที่สุดแล้ว ร่วมกับอัลกอริทึม Hoare partition มันเป็นหนึ่งในอัลกอริทึมพื้นฐานที่เขียนให้ถูกเป๊ะโดยไม่พลาดได้ยากที่สุด

    • ลองทดสอบดูโดยให้ Claude Sonnet เขียนโค้ด Python ของ binary search ที่ไม่มีบั๊ก

    def binary_search(arr, target):
    left = 0
    right = len(arr) - 1
    while left <= right:
        mid = left + (right - left) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            left = mid + 1
        else:
            right = mid - 1
    return -1

    แล้วก็ตรวจด้วย test case หลายแบบกับอาร์เรย์ตัวอย่าง

    • พอรู้ว่า binary search ขึ้นชื่อเรื่องบั๊กจาก best practice ที่ผิด ๆ ก็เลยท้าทายตัวเองว่าจะใส่ implementation แรกที่ไม่มีบั๊กลงในหนังสือ เขียนอย่างระวังมากแล้วแต่ก็ยังมีบั๊กอยู่ จนน่าขำ โชคดีที่ระบบ feedback ล่วงหน้าของ Manning ช่วยให้แก้ก่อนพิมพ์ได้

    • เวลาเขียน binary search แบบซ้าย/ขวา ฉันมักเขียนโดยจำค่า “ค่าที่ดีที่สุดจนถึงตอนก่อนหน้า” ไว้เสมอ คล้ายแนวทางของ lower_bound, upper_bound ใน C++ ใช้โครงสร้าง while (l < r) หา midpoint แล้วตรวจตำแหน่งปัจจุบันเพื่อปรับช่วงให้เหมาะสม เช่น ถ้าเป็น upper_bound ก็ขยับขอบซ้ายขึ้น ถ้าเป็น lower_bound ก็ลดขอบขวาลง ช่วงนี้กลับไปทำ leetcode หลังจากห่างไปนาน สมองเลยตื้อ ๆ รูปแบบอาจเละหน่อย

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

  • ถ้าอยากเป็นโปรแกรมเมอร์ที่ดีขึ้น ต้องสร้างนิสัยในการเขียน “บทพิสูจน์เล็ก ๆ” ให้กับโค้ด การทดสอบและการนิยาม type ก็คือตัวอย่างของการกระทำแบบนั้น โดยเฉพาะการเริ่มจาก test ก่อน จากนั้นค่อย type แล้วสุดท้ายจึงเขียนโค้ด ควรเขียน test ตาม acceptance criteria แต่ละข้อ และทำให้ input/output ถูกอธิบายไว้อย่างชัดเจน ถ้าเป็น API ก็สามารถทำสเปกก่อนด้วย OpenAPI หรือ GraphQL โดยระบุทุก property และ type ให้ครบ ที่ runtime ก็ตรวจสอบข้อมูลตามสเปกนี้ได้ และตัวสเปกเองก็เป็นหลักฐานว่าระบบทำงานตามที่กำหนดไว้ สรุปคือ การมี OpenAPI/GraphQL, test และ type เพื่อยืนยันว่าระบบทำงานตามเจตนาจริงเป็นเรื่องสำคัญ ถ้าออกแบบสเปกให้ดีตั้งแต่แรก ต่อให้เปลี่ยน implementation ของโค้ดได้ยืดหยุ่น ก็ยังพิสูจน์ความถูกต้องได้ด้วยสเปก สเปกสำคัญกว่าตัวโค้ดเอง

    • คุณสมบัติทั้งห้าข้อที่บทความกล่าวถึงสามารถแสดงออกได้ใน type system ที่ดี วิธีนี้ทำให้สเปกจำนวนมากกลายเป็นโค้ด และ compiler จะช่วยรับประกันความถูกต้อง อนาคตของการเขียนโปรแกรมควรเดินไปในทิศทางที่แนวทางแบบนี้กลายเป็นเรื่องปกติ OpenAPI และ type system ของ GraphQL ยังอ่อนเกินไปมาก ถ้าจะไปถึงอนาคตแบบนั้นคงต้องพัฒนาอีกสัก 50 ปี

  • ตอนเรียนมหาวิทยาลัยได้เรียนพื้นฐานทฤษฎีวิทยาการคอมพิวเตอร์ และเห็นด้วยกับเจตนาของบทความนี้ เพียงแต่ทำจริงไม่ง่าย นอกจาก precondition/postcondition แล้ว เทคนิคการพิสูจน์แบบ CS อย่าง loop invariant และ structural induction ก็ทรงพลังมาก ขอแนะนำ loop invariant, structural induction พร้อมทั้ง lecture note ของ UofT CSC236H (lecture note)

    • lecture note ของ CSC236 ชุดนี้ยอดเยี่ยมมาก และศาสตราจารย์ David Liu ก็เป็นคนที่ดีมากจริง ๆ แนะนำอาจารย์

    • มีการพูดถึง UofT ด้วย! ดีใจจัง

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

    • เจตนาแบบนี้ทำได้ง่ายในโปรเจกต์ greenfield (โดยเฉพาะเวลาที่เราเป็นคนเขียนโค้ดทั้งหมดเองล่าสุด) แต่ใน codebase จริงที่นักพัฒนาหลายคนไปแตะทั้งฟังก์ชันสารพัดและ global state มันรู้สึกยากกว่ามาก

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

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

      • โค้ดที่มี global state และถูกดูแลโดยนักพัฒนาหลายคน เปรียบได้กับผู้ป่วยที่ “มะเร็งลุกลาม” การรักษายากกว่ามาก และบางครั้งจะรอดหรือไม่ก็ขึ้นกับดวงและปัจจัยภายนอก

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

      • อ่านบทความนี้แล้วนึกถึงตัวเองที่คอยกลับมาทบทวนวิธีเขียนโค้ดอยู่เรื่อย ๆ และพยายามจัดระเบียบใหม่ให้ดีขึ้น เลยสงสัยว่านักพัฒนาอย่าง John Carmack เมื่อเวลาผ่านไปจะมองโค้ดเก่าของตัวเองว่าไม่ดีพอ และยังรู้สึกว่าตัวเองค่อย ๆ ทำได้ “ดีขึ้น” หรือเปล่า

  • แนวคิดที่ว่าโค้ดควรพิสูจน์ได้ ปรากฏชัดครั้งแรกเมื่อ Dekker แก้ปัญหา mutual exclusion ในปี 1959 มีเกร็ดน่าสนใจเกี่ยวกับเรื่องนี้ในงานเขียน EWD1303 ของ Dijkstra (ลิงก์ต้นฉบับ) และงานต่อมาของ Dijkstra ก็อาจมองได้ว่าเป็นการต่อยอดจากความเข้าใจนี้

  • การเขียนบทพิสูจน์ที่ถูกต้องนั้นยากมาก การ verification ของโปรแกรมก็ไม่ใช่เรื่องง่ายเหมือนกัน ในความเห็นของฉัน ถ้าจะพยายามพิสูจน์ด้วยมือมันไม่มีประสิทธิภาพ สิ่งที่ควรทำคือเขียนโค้ดแบบ idiomatic ให้เข้ากับภาษาและ codebase นั้น ๆ แล้วคุณแทบไม่ต้องกังวลเรื่อง invariant หรือ precondition/postcondition เลย หนังสือ “The Practice of Programming” ของ R. Pike และ B. W. Kernighan เน้นเรื่อง “simplicity, clarity, generality” ซึ่งให้ผลลัพธ์ดีมากในงานจริง อีกเรื่องที่เกี่ยวกันแต่ไม่เหมือนกันเสียทีเดียวคือ ถ้าคุณทำ competitive programming คุณจะต้องฝึกเทคนิคที่ช่วยรับประกันความถูกต้องของโค้ดอย่างจริงจัง ถึงจะไปถึงระดับถัดไปได้

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

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

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

    • สำหรับความถูกต้องของโค้ด ไม่มีทางลัดอื่นนอกจากต้องเขียนมันให้ถูกต้อง ถึงจะยากก็ต้องเขียนให้ถูก

    • ถ้ากลับประโยคแรกของคุณอีกแบบ จะได้ว่าหากมี abstraction ที่เหมาะสม (กล่าวคือโค้ดแบบ idiomatic ที่เหมาะกับภาษา/โค้ดเบส) การ verification ของโปรแกรมจะง่ายขึ้น เพราะใน abstraction ที่เหมาะสม เราไม่จำเป็นต้องคอยคิดเรื่อง loop invariant เป็นต้น ดังนั้นจากความถูกต้องของโค้ด การพิสูจน์ก็จะตามมาได้โดยตรง

  • ความเป็น mutable/immutable ก็เป็นคุณสมบัติสำคัญเช่นกัน ถ้าทำให้ state ไม่เปลี่ยนแปลงได้มากที่สุด ก็จะลดความซับซ้อนได้ทั้งในงาน multithreading และในการอนุมานสถานะของโปรแกรม

    • มีพูดเรื่องนี้อยู่ในบทความต้นฉบับแล้ว

  • ตอนเป็นนักศึกษาปริญญาตรีที่ Carnegie Mellon ในยุค 80 ได้รับการสอนหลักการแบบนี้อย่างชัดเจน และมันช่วยชีวิตฉันไว้มากตลอดมา โดยเฉพาะตอนที่ได้เรียนว่าการเรียกซ้ำและการอุปนัยเป็นสิ่งเดียวกัน ฉันก็เริ่มเข้าหาอัลกอริทึมแบบ recursive ได้อย่างเป็นระเบียบ แทนที่จะใช้วิธี “ลองมั่วไปเรื่อยจนกว่าจะได้คำตอบ”

    • เพิ่งได้เรียนวิชานั้นไม่นานนี้เอง และพอเรียน functional programming ก็ยิ่งรู้สึกกระจ่างมากขึ้น