Salt เป็นภาษาโปรแกรมสาย systems ตัวใหม่ที่ทำเรื่องแปลกอย่างหนึ่ง คือฝังโปรแกรมพิสูจน์ทางคณิตศาสตร์ไว้ในคอมไพเลอร์เลย ผลคือคอมไพเลอร์จะไม่ยอมคอมไพล์โค้ดของเรา จนกว่าจะพิสูจน์ได้ว่าโค้ดนั้นไม่มีทางเข้าถึง array เกินขอบเขต ไม่ใช่แค่ทดสอบแล้ว "น่าจะไม่หลุด" แต่พิสูจน์เป็นคณิตศาสตร์ว่า "เป็นไปไม่ได้ที่จะหลุด" ที่แปลกกว่านั้นคือผู้สร้างเคลมว่ามันทำแบบนี้ได้โดยไม่ต้องยอมเสียความเร็ว วัดเองแล้วได้พอ ๆ กับภาษา C ที่คอมไพล์แบบเร่งความเร็วเต็มที่ด้วย clang -O3

เรื่องนี้น่าสนใจเพราะปัญหาที่มันเข้าไปจัดการ คือปัญหาที่นักพัฒนาสาย C เจอกันมาหลายสิบปี การอ่านหรือเขียน array เกินขอบเขต (เข้าถึงตำแหน่ง index ที่ไม่มีอยู่จริง) คือต้นเหตุคลาสสิกของโปรแกรมแครชและช่องโหว่ buffer overflow และปัญหาแบบนี้มักไม่โผล่ตอนเราเขียนโค้ด แต่ไปโผล่ตอนโปรแกรมรันต่อหน้าผู้ใช้แล้ว Salt เลยพยายามย้ายการดักปัญหานี้มาไว้ก่อนหน้านั้น

บั๊กที่มาโผล่ตอนรัน ไม่ใช่ตอนเขียน

ลองเทียบสามภาษาจากโค้ดบรรทัดเดียวกัน คือการอ่านค่าจาก arr[i] ที่ i หลุดขอบ array

ในภาษา C มันคือ undefined behavior คอมไพเลอร์ไม่ทัก ตอนรันก็ไม่มีอะไรมาห้าม โปรแกรมอาจอ่านค่าขยะออกมา อาจไปทับหน่วยความจำส่วนอื่น หรือกลายเป็นช่องให้คนเจาะระบบ ส่วนภาษา Rust จะดักปัญหาเดียวกันนี้ได้ตอนรัน คือโปรแกรม panic แล้วหยุดตัวเองอย่างปลอดภัย ซึ่งก็ยังเป็นการหยุดหลังจากโปรแกรมเริ่มรันไปแล้วอยู่ดี

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

เขียนเงื่อนไขความปลอดภัย แล้วให้ Z3 พิสูจน์

หัวใจของกลไกนี้คือโปรแกรมพิสูจน์ชื่อ Z3 ซึ่งเป็น SMT solver จาก Microsoft Research พูดง่าย ๆ คือโปรแกรมที่มีหน้าที่ตอบคำถามว่า "เงื่อนไขนี้เป็นจริงเสมอไหม" ในรูปแบบของโจทย์คณิตศาสตร์ Salt เอา Z3 นี้มาฝังไว้ในคอมไพเลอร์โดยตรง

วิธีใช้คือเราเขียนเงื่อนไขความปลอดภัยกำกับไว้หน้าฟังก์ชันด้วยคีย์เวิร์ด requires(...) ตัวอย่างจริงบนหน้าเว็บ salt-lang.dev เป็นฟังก์ชันวาดพิกเซลลงจอ ที่เขียนกำกับไว้ประมาณนี้

fn set_pixel(x: i32, y: i32, ...)
    requires(x >= 0 && x < self.width && y >= 0 && y < self.height)

บรรทัด requires(...) นั้นแปลว่า "ฟังก์ชันนี้จะทำงานก็ต่อเมื่อ x, y อยู่ในกรอบจอเท่านั้น" พอถึงตอน build คอมไพเลอร์ก็ส่งเงื่อนไขนี้ให้ Z3 แล้ว Z3 จะพิสูจน์ว่าตำแหน่งหน่วยความจำที่ฟังก์ชันคำนวณออกมา ไม่มีทางหลุดออกนอกกรอบ framebuffer ได้เลย ไม่ว่าจะป้อนค่าอะไรเข้าไป และโค้ดจะทำงานตามเงื่อนไขไหน

ผลลัพธ์มีสองทาง ถ้า Z3 พิสูจน์ได้ว่าเงื่อนไขจริงเสมอ คอมไพเลอร์จะตัดการตรวจขอบเขตตอนรันออกไปเลย โปรแกรมที่ได้จึงทำงานเร็วเท่ากับตอนที่ไม่มีการตรวจความปลอดภัยนั้นอยู่ แต่ถ้า Z3 พิสูจน์ไม่ได้ การคอมไพล์จะล้มเหลว พร้อมชี้ตัวอย่างที่ทำให้เงื่อนไขไม่ผ่าน คือบอกเป็นค่าจริง ๆ เลยว่าถ้าใส่ค่านี้เข้าไปแล้วมันจะหลุดขอบ จุดที่ต่างจากเครื่องมือพิสูจน์แบบเดิมคือ ไม่มีเครื่องมือแยก ไม่มีขั้นตอน verify ต่างหาก เพราะ requires() / ensures() เป็นไวยากรณ์ของภาษาเองอยู่แล้ว

ปลอดภัยได้โดยไม่มี GC และไม่มี borrow checker

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

ปกติแล้ว ความปลอดภัยเรื่องหน่วยความจำมักต้องแลกมาด้วยอะไรบางอย่าง ภาษาที่มี garbage collector ต้องยอมให้โปรแกรมมีจังหวะหยุดเพื่อคืนหน่วยความจำที่ไม่ได้ใช้แล้ว ส่วน Rust ได้ความปลอดภัยมาจาก borrow checker ที่นักพัฒนาหลายคนบอกว่าต้องออกแรงสู้กับมันพอสมควร แต่ Salt เคลมว่าไม่ใช้ทั้งสองอย่าง มันจัดการหน่วยความจำด้วยโมเดล Arena คือจองพื้นที่เป็นก้อน หยิบ Slice ที่รู้ขอบเขตของตัวเองออกมาใช้ แล้วคืนทั้งก้อนทีเดียวจบ ไม่ต้องมานั่งคืนทีละชิ้น คอมไพเลอร์จะปฏิเสธตั้งแต่ตอน build ถ้ามี reference ตัวไหนยังถูกใช้อยู่หลังจากก้อนหน่วยความจำของมันถูกคืนไปแล้ว ส่วนขอบเขตที่ Z3 ใช้ตรวจการเข้าถึง array ก็ติดมากับตัว Slice นี่เอง

เรื่องความเร็ว หน้าเว็บของโปรเจกต์พาดหัวไว้ว่า "เร็วเท่ากับ clang -O3 เป๊ะ ๆ บน 28 benchmark" (วัดบนเครื่อง Apple M4) แต่ถ้าไปดูตัวเลขละเอียดที่ผู้สร้างให้ไว้เอง ผลจริงกลับไม่ได้เร็วเท่ากันทุกกรณี บนชุดทดสอบ 21 อัลกอริทึม Salt ทำความเร็วได้เท่ากับ C หรือเร็วกว่า C อยู่ 19 จาก 21 ตัว งานที่จองหน่วยความจำเยอะ ๆ อย่าง hashmap หรือ LRU กลับ ชนะ C ไป 2 ถึง 10 เท่าเพราะโมเดล Arena ส่วนงานที่เน้นคำนวณล้วน ๆ อย่าง matmul หรือ sieve ทำได้ที่ประมาณ 0.9 ถึง 1.0 เท่าของ C คือช้ากว่านิดหน่อย เพราะฉะนั้นจะบอกว่า "เร็วเท่า C เป๊ะทุกกรณี" ก็ไม่ถูกซะทีเดียว ผลทดสอบไม่ได้สม่ำเสมอทุกงาน และตัวเลขทั้งหมดนี้เป็นการวัดของผู้สร้างเอง ยังไม่มีใครภายนอกไปลองวัดซ้ำเพื่อยืนยัน

เบื้องหลังการทำงาน Salt จะคอมไพล์ผ่าน MLIR (โครงสร้างพื้นฐานของคอมไพเลอร์ตัวเดียวกับที่ TensorFlow และ PyTorch ใช้) แล้วลงไปเป็น LLVM (ชุดเครื่องมือคอมไพเลอร์ที่หลายภาษาใช้ร่วมกัน) รองรับทั้ง x86-64 และ ARM64

ของจริงที่ผู้สร้างเขียนโชว์

เพื่อให้เห็นว่ามันใช้เขียนระบบจริงได้ ไม่ใช่แค่ตัวอย่างสาธิตเล่น ๆ ผู้สร้างเขียนระบบจริงหลายตัวด้วย Salt แล้ววัดผลเอง โดยแต่ละตัวมี Z3 คอยพิสูจน์ว่าการเข้าถึง array ทุกจุดไม่หลุดขอบ

• Lettuce คือ in-memory store ที่เข้ากันได้กับ Redis (ฐานข้อมูลในหน่วยความจำที่ใช้กันแพร่หลาย) เขียนด้วย 567 บรรทัด zero dependency ผู้สร้างเคลมว่ามันทำความเร็วได้เท่ากับ Redis หรือเร็วกว่า Redis ในทุกระดับ concurrency ที่ทดสอบ ตั้งแต่ 1 ถึง 100 client
• Basalt คือ engine รัน Llama 2 (โมเดลภาษา AI) เขียนราว 600 บรรทัด ได้ประมาณ 870 tok/s ซึ่งผู้สร้างวัดว่าใกล้เคียงกับเวอร์ชันภาษา C
• KeuOS Train คือตัวเทรน MNIST อ่านตัวเลขลายมือ เขียน 188 บรรทัด ได้ความแม่นยำ 97%
• KeuOS คือ OS microkernel ที่บูตบนเครื่อง x86 จริงได้ โดยไม่พึ่ง C runtime หรือ libc เลยสักตัว

ถ้าอยากเห็นเรื่อง "ปลอดภัยแต่ยังเร็ว" แบบจบในไฟล์เดียว Lettuce คือตัวที่ดูง่ายสุด แต่ถ้าอยากรู้ว่ามันไปได้ไกลแค่ไหน ก็ต้องดู KeuOS ที่เป็นระดับเคอร์เนลทั้งตัว แต่ต้องจำไว้ว่า ทั้งหมดนี้เป็นงานที่คนคนเดียวเขียนและวัดผลเอง

ไม่ใช่แค่เรื่องของ Salt ภาษาเดียว

ถ้ามองภาพรวม เรื่องที่น่าสนใจจริง ๆ ไม่ใช่ภาษาใดภาษาหนึ่ง สิ่งที่ Salt ทำมีชื่อเรียกว่า formal verification หรือการพิสูจน์ความถูกต้องของโปรแกรมด้วยคณิตศาสตร์ แทนที่จะหวังว่าเทสต์จะไปเจอบั๊กเอง

แนวคิดนี้ไม่ใช่ของใหม่ มันอยู่ในงานวิจัยและงานสาย safety-critical มาหลายสิบปีแล้ว ตัวอย่างที่มีนักพัฒนาคนหนึ่งหยิบมาเทียบคือ SPARK ซึ่งเป็น subset ของภาษา Ada ที่ใช้ในงานการบินและกลาโหมมาตั้งแต่ปลายยุค 1980 และใช้ Z3 พิสูจน์เงื่อนไขจาก contract คล้าย ๆ กัน สิ่งที่กำลังเปลี่ยนไปคือเครื่องมือพวกนี้เริ่มขยับจากห้องแล็บของผู้เชี่ยวชาญ มาอยู่ใน toolchain ที่นักพัฒนาทั่วไปหยิบมาใช้ได้ Salt เป็นหนึ่งในสัญญาณที่เห็นได้ชัดของการเปลี่ยนแปลงนี้

สิ่งที่ต้องระวังไว้ก่อนตื่นเต้น

ข้อควรระวังในเรื่องนี้สำคัญพอ ๆ กับสิ่งที่ผู้สร้างเคลมไว้ และมีอยู่หลายประเด็น

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

ประเด็นที่สองคือข้อจำกัดของตัว Z3 เอง ตอนนี้มันจัดการเลขจำนวนเต็ม bit-vector และจำนวนจริงได้ดี แต่รองรับ string กับ quantifier ได้แค่บางส่วน และถ้าโจทย์พิสูจน์ตัวไหนหาคำตอบไม่ทันภายใน 100ms Salt จะข้ามการตรวจนั้นและบันทึกไว้ ไม่ใช่แอบถือว่าปลอดภัยเงียบ ๆ

ประเด็นที่สามคือตัวโปรเจกต์เอง Salt ยัง pre-1.0 ดูแลโดยนักพัฒนาคนเดียวที่ทำเป็นงานอดิเรกนอกเวลางาน ตัวผู้สร้างเองก็บอกตรง ๆ ว่ามันยังเป็นของทดลอง ยังไม่พร้อมเอาไปใช้งานจริง ชุดไลบรารีมาตรฐาน (standard library) ยังไม่ครบ และข้อความ error จากขั้นตอน Z3 บางทีก็อ่านยาก ในกระทู้ที่ผู้สร้างเปิดให้นักพัฒนาคนอื่นเข้ามาถาม-ตอบ มีคนตั้งข้อสังเกตว่าเอกสารอ่านแล้วเหมือนสร้างด้วย AI และตัว spec ยังไม่ปะติดปะต่อ อีกทั้งยังไม่มีคนนอกทีมหรือ beta tester มาลองใช้จริง ผู้สร้างก็ยอมรับว่าใช้ AI เป็นแกนหลักในการพัฒนาจริง และกำลังทยอยแก้เอกสารอยู่

ประเด็นสุดท้าย ตัวเลขทุกตัวในนี้ ไม่ว่าจะเร็วเท่า clang -O3 หรือชนะ Redis ล้วนเป็นการวัดของผู้สร้างเองบนฮาร์ดแวร์เฉพาะที่ใช้ทดสอบ ยังไม่มีใครภายนอกไปลองวัดซ้ำเพื่อยืนยัน เสียงจากนักพัฒนาคนอื่นเองก็ยังกังขา ไม่ได้ตื่นเต้นถึงขั้นมองว่ามันเสร็จสมบูรณ์พร้อมใช้แล้ว

คำถามที่น่าจับตาจึงไม่ใช่ว่า Salt จะไปแทน C หรือ Rust ได้ไหม เพราะตอนนี้ยังห่างจากจุดนั้นมาก แต่เป็นว่าการที่คอมไพเลอร์หันมาถามว่า "พิสูจน์ให้ดูก่อนสิ ว่ามันปลอดภัยจริง" ก่อนจะยอมปล่อยให้โค้ดไปรัน กำลังค่อย ๆ กลายเป็นเรื่องที่เห็นได้บ่อยขึ้นเรื่อย ๆ

ที่มา:

• Salt: Systems programming, mathematically verified — salt-lang.dev
• การพูดคุยในกระทู้ Show HN: Salt — Hacker News