Bend 2 มาแล้ว: ภาษาที่ให้คุณเขียน 'กฎ' แล้วบังคับให้ AI พิสูจน์ว่าโค้ดไม่ละเมิด — type checker เร็วกว่า Rocq 20 เท่า แต่ตัวเลขบนหน้าเว็บมีข้อควรอ่าน

คำถามที่ทุกทีมที่ปล่อย coding agent ลง production เจอเหมือนกันหมดคือ: จะเชื่อโค้ดที่เราไม่ได้อ่านได้อย่างไร? เทสต์ก็เขียนโดย AI ตัวเดียวกัน code review ก็ทำโดย AI อีกตัว สุดท้ายเราก็ได้แต่หวังว่าไม่มีอะไรพัง

Bend 2 เสนอคำตอบที่ต่างออกไป: บังคับให้ AI ส่งคำพิสูจน์ทางคณิตศาสตร์มาด้วย ทีม HigherOrderCO ย้ายรีโปไปที่ bendlang/bend เมื่อ 16 ก.ย. และปล่อยเวอร์ชัน 2.0.4 กับ 2.0.5 ตามมาในวันที่ 17 ก.ย. ตัวโปรเจกต์อยู่ใต้ Apache-2.0 มีดาวราว 21,000 ดวง (สืบทอดมาจาก Bend รุ่นแรกที่เปิดตั้งแต่ปี 2023) และขึ้นอันดับต้น ๆ ของ Hacker News ทันทีในวันเดียวกัน

LAWS.bend คือ AGENTS.md ที่มีคณิตศาสตร์ค้ำ

หัวใจของ Bend 2 คือไฟล์ชื่อ LAWS.bend ที่คุณประกาศกฎที่แอปห้ามละเมิด เมื่อกฎถูกประกาศแล้ว compiler จะเรียกร้องคำพิสูจน์ทุกครั้งที่โค้ดถูกแก้ ตัวอย่าง ที่เขาเอามาโชว์คือเกมที่มีกฎเดียว — “ชนะไม่ได้”:

# LAWS.bend
law you_cant_win:                           # "winning is impossible"
  for moves: List<Game.Move>                # ลำดับการเดินแบบไหนก็ได้
  board = Game.replay(Game.start(), moves)  # เล่นซ้ำจากจุดเริ่มต้น
  {Game.is_won(board) == False{} : Bool}    # ต้องไม่มีทางชนะ

จากนั้นสั่ง “Claude ทำให้กระดานวนรอบ” — เดโมของเขาแสดงว่าถ้าไม่มี LAWS.bend บั๊กที่ทำให้เดินทะลุขอบไปหยิบธงได้ถูก merge เข้าไปเรียบร้อย แต่ถ้ามี LAWS.bend AI ต้องลองใหม่จนกว่าจะพิสูจน์ได้ว่ากฎยังอยู่ (ในเดโมมันเลือกสร้างกำแพงที่ขอบไกล) สโลแกนของเขาคือ: LAWS.bend คือ AGENTS.md ที่มี proof ค้ำ และ “make no mistakes” กลายเป็นสิ่งที่ type-check ได้

วิธีใช้ในโปรเจกต์จริงเรียบง่ายมาก — ติดตั้งแล้วเติม 4 บรรทัดนี้ลง AGENTS.md:

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

ตัวภาษาเองเป็น dependently typed + affine ตรวจแบบ bidirectional pass เดียว มีเปเปอร์สองฉบับอยู่ในรีโป (BendTT ว่าด้วย type theory และ BendRT ว่าด้วย runtime ขนาน) และที่น่าสังเกตคือ core ของภาษาถูก mechanize ไว้ใน Lean ที่ไฟล์ bend2/bend.lean

ตัวเลข: อันไหนจริง อันไหนต้องอ่านละเอียด

Bend วาง benchmark pin ไว้ในรีโปเป็นไฟล์ข้อความ (bench/*/_pin_/apple_m4_max.txt) ซึ่งดีมาก เพราะเราตรวจได้เอง แทนที่จะดูแค่กราฟบนหน้าเว็บ ผลบน Apple M4 Max มีดังนี้

เรื่อง checker — คำโฆษณาจริง และจริงแบบขาดลอย

bench	Isabelle	Agda	Lean	Rocq	Bend
defs_12800	>300s	>300s	36.177s	5.985s	0.295s
generics_3200	>300s	>300s	19.214s	6.038s	0.384s
proofs_3200	>300s	>300s	>300s	9.526s	0.834s
trees_400	8.475s	3.266s	1.335s	1.339s	0.606s

เร็วกว่า Rocq ราว 11–20 เท่า และเร็วกว่า Lean 50–120 เท่าในเคสที่ Lean ยังวิ่งจบ นี่คือสิ่งที่ทำให้ไอเดียทั้งหมดใช้งานได้จริง — proof assistant ทั่วไปใช้เวลาเป็น นาที ซึ่งแปลว่า agent จะรัน bend PROOF.bend หลังแก้ทุกครั้งไม่ไหว แต่ถ้าต่ำกว่า 1 วินาที มันกลายเป็นเรื่องปกติได้ (หมายเหตุ: pin ของ checker ลงวันที่ 9 ก.ย. และ ตัวเลข Isabelle เป็นของเก่าจาก 2 ก.ย. ที่ไม่ได้วัดใหม่ — เขาระบุไว้เองในไฟล์)

เรื่อง runtime — ตรงนี้ต้องอ่านให้ละเอียดกว่าที่หน้าเว็บบอก

หน้าแรกเขียนว่า “บนคอร์เดียว มันวิ่งเกือบเร็วเท่า C” อ่านจาก pin จริงแล้ว คำว่า “เกือบ” ทำงานหนักพอสมควร — SEQ-CPU ของ Bend ช้ากว่า C ใน 15 จาก 16 เบนช์ มีเพียง tree-matmul ที่ชนะ (2.064s เทียบ 2.964s) ส่วนใหญ่ช้ากว่า ประมาณ 1.05–1.5 เท่า (เช่น terrain 2.225s เทียบ 2.198s แทบเท่ากัน, queens 5.406s เทียบ 3.599s) แต่มีเคสที่ห่างจริง ๆ คือ hashmap — 2.741s เทียบกับ C ที่ 0.622s หรือช้ากว่า 4.4 เท่า

พูดให้เป็นธรรม: สำหรับภาษาที่มี dependent types และ proof checking อยู่ในตัว การอยู่ห่างจาก C แค่ 10–50% บนคอร์เดียวถือว่าน่าประทับใจมาก (TypeScript ในตาราง เดียวกันช้ากว่า 3–8 เท่า) แต่ประโยคว่า “as fast as hand-written C” ควรอ่านว่า “อยู่ในระดับเดียวกับ C” ไม่ใช่ “เท่ากันหรือดีกว่า”

เรื่อง GPU — ไม่ใช่ปุ่มวิเศษ

ตัวเลข PAR-GPU สวยมากในงานที่แตกขนานได้จริง: gameoflife จาก 7.803s (คอร์เดียว) เหลือ 0.063s คือเร็วขึ้น 124 เท่า, mandelbrot 0.057s, nbody 0.059s แต่มี 4 เบนช์ที่ GPU ช้ากว่า CPU 16 คอร์: lexer (1.075s บน GPU เทียบ 0.198s บน PAR-CPU), queens (0.933s เทียบ 0.455s), symreg (0.529s เทียบ 0.266s) และ hashmap (0.521s เทียบ 0.238s) — ซึ่งสมเหตุสมผล เพราะงานที่มี branch เยอะหรือ memory access ไม่สม่ำเสมอไม่เข้ากับ GPU อยู่แล้ว

ส่วน PAR-CPU นั้นสม่ำเสมอกว่ามาก — เร็วขึ้นจากคอร์เดียวราว 9–12 เท่าแทบทุกเบนช์ โดยไม่ต้องเขียน thread หรือ lock เอง ซึ่งอาจเป็นคุณค่าที่ใช้งานได้จริงที่สุด ของ Bend ในวันนี้

สิ่งที่ควรรู้ก่อนพิมพ์ curl | sh

การติดตั้งคือ curl -fsSL https://bend-lang.com/install.sh | sh — เราอ่าน สคริปต์นั้นแล้ว มีสามอย่างที่ควรรู้ก่อนรัน:

1. มันติดตั้ง Bun ให้ด้วย ถ้าเครื่องคุณยังไม่มี (curl … bun.sh/install | bash อีกชั้นหนึ่ง) ส่วนการคอมไพล์เป็น binary ต้องมี clang 19 ขึ้นไป และถ้าจะใช้ GPU ต้องมี Metal (macOS) หรือ CUDA 12 (Linux)
2. มันส่ง telemetry ทุกครั้งที่รัน — launcher จะ POST {id, ver, os, arch, cmd, exit, ms} ไปที่ bend-lang.com/ping เป็น background ปิดได้ด้วย BEND_NO_TELEMETRY=1 ซึ่งเขาเขียนบอกไว้ในคอมเมนต์ของสคริปต์ตรง ๆ แต่ไม่ได้ โฆษณาบนหน้าเว็บ
3. มันอัปเดตตัวเองเงียบ ๆ — คำตอบจาก /ping บอกเวอร์ชันล่าสุด แล้วรันถัดไป จะโหลด tarball ใหม่ ตรวจ sha256 แล้วสลับ symlink current ทีมที่ต้องการ build reproducible ควรตรึงเวอร์ชันเอง ไม่ใช่ปล่อยให้ launcher จัดการ

อีกเรื่องที่น่าสนใจในเชิงวัฒนธรรม: ไฟล์ AGENTS.md ของรีโปเองระบุว่า bend2/bend.ts (ตัวภาษา: parser, theory, checker) เขียนโดยมนุษย์ ห้ามแก้ ซึ่งโดยนัยแปลว่าส่วนที่เหลือไม่ใช่ และคอมมิตล่าสุดเมื่อเช้าวันที่ 18 ก.ย. มีข้อความว่า “The papers’ AI disclosure ends with: Human paper soon™” — โปรเจกต์ที่ขายเรื่องการตรวจสอบโค้ด AI ก็สร้างด้วย AI เป็นส่วนใหญ่ และเปิดเผย เรื่องนี้เอง

มุมมอง AI Curator

Bend 2 ตั้งคำถามที่ถูกต้องที่สุดในยุคนี้ และเป็นคำถามที่เราเชื่อว่าจะสำคัญขึ้น เรื่อย ๆ: เมื่อโค้ดถูกเขียนเร็วกว่าที่มนุษย์อ่านทัน อะไรคือสิ่งที่ยังตรวจสอบได้? คำตอบแบบ “เขียนเทสต์เยอะ ๆ” ไม่พอ เพราะเทสต์ก็คือ AI เขียน และเทสต์พิสูจน์ได้แค่ เคสที่นึกออก ส่วน LAWS.bend พิสูจน์สำหรับ ทุก ลำดับ input ที่เป็นไปได้ — มันเป็นคนละระดับของการรับประกันจริง ๆ

แต่ต้องพูดให้ชัดว่าข้อจำกัดอยู่ตรงไหน: กฎครอบคลุมได้เฉพาะสิ่งที่คุณ formalize เป็นคณิตศาสตร์ได้ “ผลรวมยอดเงินต้องเป็นศูนย์”, “list_sort คืนค่าเรียงขึ้นเสมอ”, “ห้ามเข้าถึง array นอกขอบเขต” — พวกนี้เขียนเป็นกฎได้ แต่ “UI ต้องใช้งานง่าย”, “อย่า log ข้อมูลส่วนบุคคล”, “อย่าเรียก API ของ vendor เกินโควตา” ส่วนใหญ่ formalize ไม่ได้ในทางปฏิบัติ และบั๊กที่ทำให้ระบบ production ล่มจริง ๆ ก็มักอยู่ ในกลุ่มหลังมากกว่ากลุ่มแรก Bend ไม่ได้แก้ทุกอย่าง มันยกพื้นของสิ่งที่พังไม่ได้ ให้สูงขึ้นเท่านั้น — ซึ่งก็มีค่ามากอยู่แล้ว

อีกอุปสรรคที่ใหญ่กว่าเรื่องเทคนิคคือ การเขียนกฎที่ถูกต้องนั้นยาก งานวิจัย ด้าน formal methods เจอปัญหานี้มา 40 ปี: ถ้า spec ผิด proof ที่ถูกต้อง 100% ก็รับประกันสิ่งที่ผิด และตอนนี้ Bend แนะนำให้ “ให้ AI เขียน LAWS.bend ให้” ซึ่งย้ายปัญหาไปหนึ่งชั้น ไม่ได้ทำให้มันหายไป ทีมที่จะใช้จริงควรอ่านกฎเอง — ข่าวดีคือกฎสั้นกว่าโค้ดมาก จึงพอ review ได้ ต่างจาก implementation

สำหรับทีมไทย เราไม่แนะนำให้ย้าย production ไปเขียนด้วย Bend วันนี้ — เขาเองก็ เขียนว่า “Bend is young: if anything goes wrong, ask it to open an issue” และ ยังไม่มี release tag เป็นทางการบน GitHub เลยสักอัน ยังไม่มี ecosystem ไลบรารี ยังทำงานได้ดีเฉพาะฝั่ง back-end บน Linux/macOS แต่สิ่งที่ควรทำคือ ยืมแนวคิด — ในสแตกที่คุณใช้อยู่ตอนนี้ มีตรงไหนบ้างที่ย้ายจาก “เทสต์” ไปเป็น “property test หรือ type-level invariant” ได้? การเพิ่ม property-based test (Hypothesis, fast-check, QuickCheck) ลงในฟังก์ชันที่ agent แตะบ่อยที่สุด ให้ผลตอบแทนคล้ายกันโดยไม่ต้องเปลี่ยนภาษา และทำได้ในบ่ายวันเดียว

สุดท้าย เราชอบที่ทีมนี้วาง benchmark pin เป็นไฟล์ข้อความในรีโปพร้อมวันที่และ commit hash — มันเปิดโอกาสให้คนนอกเถียงกับตัวเลขของเขาได้ อย่างที่เราเพิ่งทำ ไปในบทความนี้ วงการ AI จะดีขึ้นเยอะถ้าทุกเจ้าทำแบบนี้แทนที่จะปล่อยแค่กราฟ

แหล่งข่าว

• Bend — เว็บไซต์ทางการ
• bendlang/bend — GitHub (Apache-2.0)
• Benchmark pin: runtime บน Apple M4 Max (17 ก.ย. 2026)
• Benchmark pin: checker เทียบ Isabelle, Agda, Lean, Rocq