กาเบรียลา โมเรย์รา CEO ของ Quint ที่ Informal Systems – ซีรีส์สัมภาษณ์

กาเบรียลา โมเรย์รา ซีอีโอของ Quint ที่ Informal Systems เป็นวิศวกรวิจัยที่เชี่ยวชาญด้านภาษาโปรแกรมมิ่งและวิธีการทางรูปแบบ โดยมุ่งเน้นในการสร้างเครื่องมือที่ทำให้การยืนยันระบบที่ซับซ้อนเป็นไปได้มากขึ้นสำหรับวิศวกร เธอนำการพัฒนา Quint ซึ่งเป็นภาษาสำหรับระบุแบบใหม่ที่ใช้ TLA+ โดยที่เธอพัฒนาภาษาและเครื่องมือต่อไป การทำงานของเธอครอบคลุมการยืนยันแบบรูปแบบ การวิเคราะห์แบบคงที่ และเครื่องมือสำหรับนักพัฒนา และเธอยังได้เขียนบทความทางวิชาการด้านวิธีการทางรูปแบบ ซึ่งสะท้อนถึงการผสมผสานระหว่างการออกแบบเชิงปฏิบัติและความลึกทางทฤษฎี

Quint ซึ่งพัฒนาและดูแลโดย Informal Systems เป็นภาษาสำหรับระบุแบบสมัยใหม่ที่ออกแบบมาเพื่อสร้างแบบจำลอง ทดสอบ และยืนยันระบบที่ซับซ้อน เช่น เครือข่ายแบบกระจาย บล็อกเชน และฐานข้อมูล โดยสร้างขึ้นบนพื้นฐานของ Temporal Logic of Actions (TLA) Quint มีการแนะนำไวยกรณ์ที่เป็นมิตรกับนักพัฒนามากขึ้น พร้อมด้วยเครื่องมือขั้นสูง เช่น การตรวจสอบประเภท การจำลอง และการตรวจสอบแบบจำลอง ซึ่งช่วยให้วิศวกรสามารถตรวจจับข้อผิดพลาดของระบบก่อนที่จะนำไปใช้งานจริง แพลตฟอร์มนี้เน้นไปที่การระบุแบบที่สามารถนำไปใช้ได้จริง ทำให้นักพัฒนาสามารถอธิบายพฤติกรรมของระบบได้ไม่เพียงแต่การเขียนโค้ดเท่านั้น แต่ยังสามารถทดสอบและสำรวจได้ด้วย

เมื่อกลับไปที่จุดเริ่มต้น สิ่งใดที่ทำให้คุณสนใจในการเขียนโปรแกรม และคุณได้พบกับวิธีการทางรูปแบบและระบบแบบกระจายอย่างไร?

ฉันชอบเล่นเกมมาก แต่คอมพิวเตอร์ของฉันไม่ดี และฉันรู้สึกว่าฉันชอบแก้ปัญหาและทำให้มันทำงานได้ ฉันลงทะเบียนเรียนวิชาวิทยาศาสตร์คอมพิวเตอร์ และฉันถูกดึงดูดไปที่ทฤษฎีและคอมไพล์เลอร์

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

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

คุณได้สร้างอาชีพของคุณโดยรอบวิธีการทางรูปแบบและภาษาโปรแกรมมิ่ง ตั้งแต่การทำงานแรกของคุณเกี่ยวกับเครื่องมือที่ใช้ TLA+ ไปจนถึงการเป็นผู้นำในการพัฒนา Quint ที่ Informal Systems สิ่งใดที่กระตุ้นให้คุณมุ่งเน้นไปที่การทำให้การยืนยันแบบรูปแบบเป็นไปได้มากขึ้น และวิสัยทัศน์นั้นได้กำหนดรูปแบบของ Quint อย่างไร?

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

Quint ไม่ได้ถูกออกแบบมาเป็นผลิตภัณฑ์ แต่เราได้สร้างมันขึ้นมาจากความจำเป็นใน Informal Systems เราเขียนสเปค TLA+ สำหรับระบบที่เราต้องการเชื่อถือมากกว่าที่เราทำ แต่มันไม่ได้ขยายออกไปนอกกลุ่มคนเล็กๆ เนื่องจากไวยกรณ์มันค่อนข้างน่ากลัวและมีสัญลักษณ์ทางคณิตศาสตร์มาก และเครื่องมือไม่ตรงตามความคาดหวังของคนส่วนใหญ่

คุณสามารถอธิบาย Quint และเหตุผลที่ภาษาสำหรับระบุแบบใหม่จำเป็นต้องมีได้อย่างไร สำหรับผู้อ่านที่ไม่คุ้นเคยกับมัน?

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

สเปค Quint คือสิ่งที่คุณสามารถนำไปใช้ได้ คุณสร้างแบบจำลองระบบเป็นเครื่องจักรสถานะ และกำหนดคุณสมบัติที่ควรตรงตาม และคุณสามารถทดสอบหรือยืนยันแบบจำลองได้ หากมีการละเมิด คุณจะได้รับตัวอย่างที่แสดงลำดับการดำเนินการที่ทำให้เกิดการละเมิดนั้น

Quint ถูกออกแบบมาเพื่อช่วยลดช่องว่างระหว่างวิธีการทางรูปแบบและวิศวกรรมซอฟต์แวร์แบบปกติ อะไรคืออุปสรรคด้านการใช้งานที่ใหญ่ที่สุดที่คุณพยายามขจัดเมื่อเทียบกับวิธีการแบบดั้งเดิม?

อุปสรรคด้านการใช้งานที่ใหญ่ที่สุดคือไวยกรณ์ นั่นคือเหตุผลที่เริ่มต้นด้วยไวยกรณ์ หลังจากแก้ไขปัญหานั้นแล้ว เราก็สามารถมุ่งเน้นไปที่ปัจจัยอื่นๆ ได้

ระบบประเภทและผลกระทบของ Quint มาเพื่อขจัดข้อผิดพลาดสเปคให้มากที่สุดก่อนที่จะเริ่มกระบวนการยืนยันปกติ และคนๆ ต่างชื่นชมคุณค่าของมันมาก

คุณได้ทำงานเกี่ยวกับการวิเคราะห์แบบคงที่และระบบประเภทด้วย อย่างไรที่ประสบการณ์เหล่านั้นได้กำหนดรูปแบบการตรวจสอบประเภทและเครื่องมือของ Quint?

สิ่งที่ฉันเรียนรู้มากที่สุดในโลกของภาษาโปรแกรมมิ่งคือว่าภาษาไม่ได้เหมือนกันเสมอไป คุณอาจได้ยินคนพูดว่ามันแค่เรื่องของการเรียนรู้ไวยกรณ์ใหม่ แต่นั่นไม่ถูกต้อง

การเขียนโปรแกรมแบบฟังก์ชันถูกแนะนำให้ฉันในตอนต้น และฉันเรียนรู้ Haskell ในเวลาเดียวกับที่ฉันเรียนรู้ C ฉันขอขอบคุณสำหรับมัน

การ教授วิธีการทางรูปแบบในฐานะผู้สอนให้คุณมีมุมมองที่เป็นเอกลักษณ์ อะไรคือความเข้าใจผิดที่พบบ่อยที่สุดเกี่ยวกับการยืนยันแบบรูปแบบที่วิศวกรมีในปัจจุบัน?

นักเรียนส่วนใหญ่ไม่เคยได้ยินเกี่ยวกับวิธีการทางรูปแบบหรือการยืนยันแบบรูปแบบมาก่อน ดังนั้นจึงไม่มีความเข้าใจผิด

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

มีความสนใจที่เพิ่มขึ้นในการผสมผสาน AI กับการพัฒนาซอฟต์แวร์ คุณเห็นบทบาทของ AI ในการช่วยให้นักพัฒนาคำนวณ ส่งเสริม หรือแม้แต่สร้างสเปคแบบอย่างโดยใช้เครื่องมืออย่าง Quint?

มีบทบาทที่สำคัญ และมันกำลังเกิดขึ้นแล้ว LLMs สามารถเขียนสเปค Quint จากคำอธิบายภาษาธรรมชาติของระบบและแม้แต่โค้ดที่มีอยู่

ในเวลาเดียวกัน Quint ยังช่วยให้นักพัฒนามั่นใจในโค้ดที่เขียนด้วย AI ฉันเชื่อมั่นว่าความมั่นใจนั้นควรมาจากความเข้าใจ ไม่ใช่การตรวจสอบแบบเวทมนตร์

เมื่อมองไปข้างหน้า สิ่งใดที่ต้องเกิดขึ้นเพื่อให้วิธีการทางรูปแบบสามารถย้ายจากความนิยมในกลุ่มเล็กๆ ไปเป็นส่วนหนึ่งของวงจรชีวิตการพัฒนาซอฟต์แวร์?

สำหรับ Quint ที่จะถูกนำมาใช้มากขึ้น มีสองสิ่งที่สำคัญ: ต้นทุนต่ำและคุณค่าสูง

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

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