Gabriela Moreira, CEO của Quint tại Informal Systems – Phỏng vấn

Gabriela Moreira, CEO của Quint tại Informal Systems, là một kỹ sư nghiên cứu chuyên về ngôn ngữ lập trình và phương pháp hình thức, với trọng tâm mạnh mẽ vào việc xây dựng các công cụ giúp xác thực hệ thống phức tạp trở nên dễ tiếp cận hơn với các kỹ sư. Cô dẫn đầu sự phát triển của Quint, một ngôn ngữ đặc tả thực thi hiện đại dựa trên TLA+, nơi cô tiếp tục duy trì và phát triển ngôn ngữ và công cụ của nó. Công việc của cô bao gồm xác thực hình thức, phân tích tĩnh và công cụ phát triển, và cô cũng đã đóng góp cho học thuật bằng cách giảng dạy phương pháp hình thức, phản ánh sự kết hợp giữa kỹ thuật thực tế và chiều sâu lý thuyết.

Quint, được phát triển và duy trì tại Informal Systems, là một ngôn ngữ đặc tả hiện đại được thiết kế để mô hình hóa, kiểm tra và xác thực các hệ thống phức tạp như mạng phân tán, blockchain và cơ sở dữ liệu. Xây dựng trên nền tảng của Logic Thời gian Hành động (TLA), Quint giới thiệu một cú pháp thân thiện với nhà phát triển hơn, cùng với công cụ tiên tiến như kiểm tra kiểu, mô phỏng và kiểm tra mô hình, cho phép các kỹ sư phát hiện lỗi hệ thống trước khi triển khai. Nền tảng này nhấn mạnh vào các đặc tả thực thi, cho phép các nhà phát triển không chỉ mô tả hành vi của hệ thống mà còn tích cực kiểm tra và khám phá nó, bắc cầu giữa sự chính xác lý thuyết và triển khai thực tế.

Trở lại bắt đầu, điều gì đầu tiên đã khơi dậy sự quan tâm của bạn đến lập trình, và bạn đã tìm thấy cách vào các phương pháp hình thức và hệ thống phân tán như thế nào?

Tôi là một người chơi game nhiệt tình với một máy tính kém, và tôi nhận ra rằng tôi thích sửa chữa các vấn đề và làm cho nó hoạt động. Tôi đăng ký khoa học máy tính và được thu hút bởi lý thuyết và trình biên dịch. 

Năm 2015, tôi được giới thiệu về các cuộc thi lập trình. Trong đó, bạn thường nhận được một số ví dụ về đầu vào và đầu ra dự kiến, và bạn viết mã để giải quyết vấn đề và làm việc cho những ví dụ đó. Tuy nhiên, sau khi bạn gửi nó để đánh giá, mã thực sự được kiểm tra với nhiều ví dụ hơn ngoài những gì họ hiển thị cho bạn. Đó là sự nhận ra rằng mã có thể hoạt động cho các kịch bản tôi thấy hoặc nghĩ về, nhưng vẫn có thể thất bại trong các trường hợp tôi chưa xem xét, đã biến lập trình thành một loại thách thức mà tôi yêu thích.

Làm việc trong ngành, tôi nhanh chóng bị thu hút bởi các hệ thống phân tán, nơi chúng tôi phải xem xét các thứ tự khác nhau của tin nhắn có thể đến, các chế độ thất bại khác nhau và một thế giới của các hành vi ẩn. Năm 2018, một đồng nghiệp đã giới thiệu tôi về một ngôn ngữ đặc tả hình thức gọi là TLA+. Tôi đã bị thu hút. Tôi ngay lập tức bắt đầu xây dựng các công cụ xung quanh TLA+ và đã làm việc trong không gian này từ đó.

Bạn đã xây dựng sự nghiệp của mình xung quanh các phương pháp hình thức và ngôn ngữ lập trình, từ công việc đầu tiên về công cụ dựa trên Logic Thời gian Hành động (TLA+) đến việc lãnh đạo sự phát triển của Quint tại Informal Systems. Điều gì đã thúc đẩy bạn tập trung vào việc làm cho xác thực hình thức trở nên dễ tiếp cận hơn, và tầm nhìn đó đã định hình thiết kế của Quint như thế nào?

TLA+ quá tốt để không được sử dụng rộng rãi trong ngành. Tôi vẫn còn khá trẻ khi tôi học về nó, và tôi sẽ tham gia các cuộc gọi với đồng nghiệp của tôi để cố gắng tìm ra các giải pháp cùng nhau, và tôi luôn tìm thấy các kịch bản mà các giải pháp của chúng tôi sẽ thất bại. Tuy nhiên, tôi luôn là hàng phòng thủ cuối cùng chống lại những kịch bản đó trong hầu hết các trường hợp. Tôi nghĩ có phải có một cách tốt hơn, ít tốn kém hơn, có giá trị hơn để giải quyết những kịch bản đó. Vì vậy, ý tưởng sử dụng các phương pháp hình thức để tạo ra các đặc tả trước khi thực hiện mã đã được tạo ra. Vì vậy, tôi bắt đầu hành trình học thuật của mình về nó, điều này đã dẫn tôi đến Informal Systems và Quint.

Quint không được hình thành ban đầu như một sản phẩm. Chúng tôi xây dựng nó xuất của sự cần thiết tại Informal Systems. Chúng tôi đã viết các đặc tả TLA+ cho các hệ thống chúng tôi cần tin cậy hơn những gì chúng tôi làm, nhưng điều đó không mở rộng quá một nhóm nhỏ các người vì cú pháp quá đáng sợ với quá nhiều biểu tượng toán học, và công cụ không đáp ứng được kỳ vọng cơ bản của mọi người. Chúng tôi sẽ hiển thị cho đồng nghiệp và các cộng tác viên bên ngoài: “nhìn vào điều tuyệt vời này tôi đã làm”, nhưng họ không thể đọc nó, và không có thời gian để học một công cụ mới.

Các lựa chọn thiết kế trong Quint tuân theo trực tiếp từ kinh nghiệm đó. Ngôn ngữ dễ đọc và nhớ. Điều đầu tiên chúng tôi xây dựng là một tiện ích mở rộng VSCode rằng突出 lỗi khi bạn nhập. Nó có kiểu và chế độ riêng biệt để tách các lớp rõ ràng. Nó có một REPL để bạn có thể khám phá tương tác, và một mô phỏng để bạn có thể nhận được phản hồi nhanh chóng và lặp lại. Nó xuất các vết theo định dạng JSON tiêu chuẩn mà máy dễ dàng phân tích. Đó là những thứ mà các lập trình viên đã mong đợi từ các công cụ của họ và mà chúng tôi cần mình. Xác thực bên dưới là logic giống như TLA+.

Tôi bị ám ảnh bởi việc làm cho các phương pháp hình thức trở nên dễ tiếp cận hơn, và việc xuất bản các công cụ là thú vị, nhưng tác động thực sự chỉ được cảm nhận nếu các nhóm kỹ sư thực sự sử dụng chúng. Còn một khoảng cách giữa những gì các công cụ có thể làm và làm thế nào hữu ích chúng cảm thấy đối với các nhà phát triển, và tôi đang làm việc để đóng khoảng cách đó.

Đối với những người đọc chưa quen với nó, bạn sẽ giải thích Quint là gì và tại sao một ngôn ngữ đặc tả mới là cần thiết bên cạnh các công cụ hiện có như TLA+?

Hầu hết các đặc tả là tài liệu. Bạn viết xuống những gì hệ thống nên làm, và bạn kiểm tra chúng bằng cách đọc chúng. Vấn đề là tài liệu sai theo những cách bạn không thể phát hiện cơ học: tên không xác định, hành vi mơ hồ, giả định ngầm định. Bạn thường phát hiện ra trong quá trình triển khai, hoặc trong sản xuất.

Một đặc tả Quint là điều bạn thực thi. Bạn mô hình hóa hệ thống như một máy trạng thái, định nghĩa các thuộc tính nó nên thỏa mãn, và chạy hoặc xác thực mô hình. Nếu có một vi phạm, bạn nhận được một ví dụ phản đối cho thấy chính xác chuỗi các bước kích hoạt nó. Điều đó thay đổi khi và làm thế nào rẻ để bắt một khiếm khuyết thiết kế.

TLA+ luôn có thể làm điều đó. Quint làm cho nó thực tế cho các kỹ sư không phải là chuyên gia về logic thời gian.

Quint được thiết kế để bắc cầu giữa các phương pháp hình thức và kỹ thuật phần mềm hàng ngày. Những rào cản về khả năng sử dụng lớn nhất bạn nhằm loại bỏ so với các phương pháp truyền thống là gì?

Thành thật, rào cản về khả năng sử dụng lớn nhất là cú pháp. Đó là lý do chúng tôi bắt đầu với cú pháp. Sau khi giải quyết vấn đề đó, chúng tôi có thể tập trung vào các yếu tố khác. Hệ thống kiểu và hiệu ứng của Quint đến để đánh dấu càng nhiều lỗi càng tốt trước khi bắt đầu quá trình xác thực thường xuyên, và mọi người đánh giá cao điều đó. Nó dẫn chúng tôi viết các đặc tả chất lượng cao hơn mà thậm chí nhiều người có thể đọc. Chúng tôi tích hợp tất cả trong các trình soạn thảo, và cung cấp chức năng cơ bản mà tất cả các nhà phát triển có quyền mong đợi.

Tác động lớn nhất sau đó là mô phỏng của chúng tôi. Nó bắt đầu như một cách để cung cấp cho mọi người phản hồi đầu tiên về hành vi của hệ thống của họ, như một nhà phát triển muốn có thể chạy mã sau khi họ viết nó. Nó thì biến thành một cách để có được sự tự tin về các đặc tả quá lớn để xác thực có thể xử lý, vì chuyên môn về việc thích nghi một đặc tả để làm cho nó khả thi cho xác thực không nên được coi là có sẵn. Mô phỏng của chúng tôi làm cho sự tự tin trở nên dễ tiếp cận hơn và chúng tôi đã sử dụng nó rộng rãi trong nhiều dự án.

Điểm đau lớn nhất của tôi với cú pháp TLA+ là tôi thường xuyên trộn lẫn các dấu gạch chéo và dấu gạch chéo thường, và bạn cần nhập những dấu đó rất nhiều. Tôi thích cú pháp Quint hơn, nhưng điều thực sự khiến tôi không thể quay lại là tất cả các công cụ.

Một trong những điểm mạnh của Quint là khả năng mô hình hóa và kiểm tra các hệ thống phân tán trước khi triển khai. Điều này thay đổi cách các kỹ sư nên nghĩ về việc xây dựng các hệ thống như blockchain hoặc cơ sở hạ tầng thời gian thực như thế nào?

Sự thay đổi lớn nhất là di chuyển xác thực sớm hơn. Leslie Lamport, người tạo ra TLA+, so sánh việc viết đặc tả trước mã với việc vẽ bản thiết kế trước công việc xây dựng. Ngay cả khi bạn đã xây dựng một thứ gì đó mà không có bản thiết kế, nó vẫn là một ý tưởng tốt để viết một bản thiết kế bây giờ và sử dụng nó để thông báo cho các thay đổi tiếp theo của bạn.

Trong ngành công nghiệp phần mềm, chúng tôi sử dụng các tệp markdown và bảng trắng. Có thể bạn có thể so sánh điều đó với việc cố gắng mô tả một tòa nhà bằng văn bản. Nó hoạt động, nhưng bạn có biết liệu kích thước tường có cộng lại không? Quint cung cấp một cách để mô tả các hệ thống mà bạn có thể ở mức cao như bạn muốn, và nhận được thông tin về hành vi và sự chính xác của nó.

Quint xây dựng trên nền tảng của TLA+, được sử dụng rộng rãi để mô tả các hệ thống phân tán. Bạn đã cân bằng giữa việc duy trì sự nghiêm ngặt lý thuyết đó và làm cho ngôn ngữ trở nên thân thiện với nhà phát triển hơn như thế nào?

Quyết định chính là hạn chế Quint đến một phần của TLA (logic đằng sau TLA+) thay vì lộ ra mọi thứ logic cho phép. TLA rất giàu biểu đạt, và một số biểu đạt đó bao gồm các toán tử không được hỗ trợ bởi bất kỳ công cụ nào, và cho phép các kết hợp mà mọi người hiểu và sử dụng sai, làm cho mọi thứ thực sự khó gỡ lỗi. Chúng tôi đã đưa ra một quyết định có chủ ý: gắn bó với những gì hầu hết các đặc tả thực tế thực sự cần, và tránh những gì có tiềm năng gây nhầm lẫn.

Hệ thống kiểu và hiệu ứng thêm các ràng buộc, nhưng các ràng buộc đó hữu ích. Chúng ngăn chặn một lớp các lỗi đặc tả mà không thú vị khi tìm thấy sau khi quá trình xác thực đã chạy. Kiểu gần như hoàn toàn được suy luận và hiệu ứng được ẩn khỏi người dùng, vì vậy điều này thêm giá trị mà không có ma sát.

Trước khi tôi học về sự tồn tại của TLA+, tôi đã làm việc nghiên cứu về hệ thống kiểu, điều đó có nghĩa là trình kiểm tra kiểu của Quint có lẽ là thành phần yêu thích của tôi để viết. Tôi nhớ uống một ly cà phê hương vị Paçoca trong những tháng đầu tiên tại Informal trong khi xem xét một số giấy về hệ thống kiểu và nghĩ “cuộc sống của tôi thật tuyệt vời”. 

Làm cho ngôn ngữ tốt để sử dụng trong khi vẫn giữ sự tương ứng với TLA+ (vì các đặc tả Quint có thể được biên dịch thành TLA+) là một bài tập về ngôn ngữ lập trình, và các cuộc thảo luận với nhóm là nguồn lực hữu ích nhất, tiếp theo là phản hồi từ người dùng sớm. Còn những cải tiến chúng tôi muốn thực hiện, và nó có thể là phần yêu thích của tôi trong công việc.

Bạn cũng đã làm việc về phân tích tĩnh và hệ thống kiểu. Những kinh nghiệm đó đã ảnh hưởng đến việc kiểm tra kiểu của Quint, công cụ và tổng thể trải nghiệm của nhà phát triển như thế nào?

Bài học lớn nhất tôi đã học trong thế giới đó là không tất cả các ngôn ngữ đều giống nhau. Bạn sẽ nghe mọi người nói rằng nó chỉ là vấn đề học một cú pháp mới, tất cả các khái niệm vẫn áp dụng, vì vậy tất cả các ngôn ngữ đều bằng nhau và nó chỉ là vấn đề về sở thích. Điều đó không đúng. Lĩnh vực ngôn ngữ lập trình có những nhà nghiên cứu tuyệt vời làm việc để thúc đẩy lĩnh vực này, và điều đó không chỉ để làm cho một ngôn ngữ trông đẹp hơn hoặc phù hợp với sở thích của họ.

Lập trình chức năng được giới thiệu cho tôi rất sớm, tôi đã học Haskell cùng lúc với C (ngôn ngữ lập trình đầu tiên của tôi), và tôi rất biết ơn điều đó. Đây là nền tảng giúp tôi thấy rằng cách ly các trạng thái đột biến và không xác định đến một lớp mỏng trong Quint, và có tất cả sự phức tạp trong các hàm thuần túy giúp ích trong nhiều yếu tố, và điều đó không chỉ là vấn đề về sở thích. Tôi không nghĩ rằng việc xây dựng Quint sẽ có hiệu quả nếu những vấn đề về sở thích được thảo luận quá thường.

Làm giáo viên giảng dạy các phương pháp hình thức cho bạn một quan điểm độc đáo. Những quan niệm sai lầm phổ biến nhất mà các kỹ sư có về xác thực hình thức ngày nay là gì?

Tốt, tôi đã dạy cho các sinh viên đại học mới bắt đầu trong ngành. Hầu hết họ chưa bao giờ nghe về các phương pháp hình thức hoặc xác thực hình thức trước đó, vì vậy không có quan niệm sai lầm! Chương trình giảng dạy được thiết kế để hầu hết họ cũng không học về các hệ thống phân tán, và khoảng một nửa trong số họ sẽ học về các luồng trong cùng một học kỳ. Tôi đã nói với họ rằng tôi cảm thấy như tôi đang dạy họ những gì một chiếc ô là tốt cho trước khi họ đã trải qua bất kỳ cơn mưa nào!

Tôi đã được thúc đẩy hơn để dạy họ cách các phương pháp hình thức và việc chỉ định hình thức một hệ thống có thể giúp chúng tôi suy nghĩ về các giải pháp và tìm các trường hợp biên, hơn là làm cho họ nghĩ rằng họ nên xác thực hình thức mọi phần mềm họ từng viết. Bài tập cuối cùng của tôi là một thiết lập trò chơi bàn cờ nơi các thứ tự mà người chơi có thể thực hiện và các thiết lập khác nhau phải được tính đến, cố gắng mô phỏng các khó khăn chúng tôi gặp phải trong các hệ thống phân tán càng nhiều càng tốt. Nó đã thành công trong việc đủ khó để họ phải sử dụng các công cụ để tìm các trường hợp biên và cải thiện các giải pháp của họ để đánh bại các con quái vật ở cuối. Hy vọng rằng khi họ đối mặt với một tình huống tương tự tại nơi làm việc một ngày nào đó, họ sẽ nhớ đến tôi. Một số người trong số họ đã làm như vậy.

Có một sự quan tâm ngày càng tăng trong việc kết hợp AI với phát triển phần mềm. Bạn có thấy vai trò của AI trong việc giúp các nhà phát triển viết, xác thực hoặc thậm chí tạo ra các đặc tả hình thức sử dụng các công cụ như Quint không?

Một vai trò đáng kể, và nó đã đang xảy ra. Khoa học máy tính lớn hơn việc viết mã, và AI mở ra cửa sổ cho các cách sử dụng hoàn toàn mới các phương pháp hình thức. Các mô hình ngôn ngữ lớn là tốt trong việc viết các đặc tả Quint từ các mô tả ngôn ngữ tự nhiên của một hệ thống và thậm chí mã hiện có. Bộ công cụ LLM của Quint có các tác nhân Claude Code lấy một mô tả tiếng Anh của một giao thức và sản xuất một đặc tả Quint mà bạn có thể chạy và kiểm tra ngay lập tức.

Đồng thời, Quint cũng giúp các nhà phát triển tin tưởng mã được viết với AI. Tôi tin mạnh mẽ rằng sự tự tin cần đến từ sự hiểu biết, không phải một số dấu kiểm ma thuật. Làm việc trên một đặc tả Quint mà thúc đẩy và kiểm tra mã thực hiện có nghĩa là các nhà phát triển vẫn có thể sở hữu và hiểu hành vi của hệ thống, giải quyết nợ nhận thức mà việc sử dụng AI có thể tạo ra và cung cấp các cách khẳng định hơn để xác thực mã được tạo.

Chúng tôi tận dụng các mô hình ngôn ngữ lớn như các công cụ ngôn ngữ viết các định nghĩa chính xác của Quint từ ý định ngôn ngữ tự nhiên, và sau đó cung cấp các công cụ Quint cho AI để nó có thể thực hiện những việc mà nó không thể làm một cách đáng tin cậy bằng chính mình, như tìm các trường hợp biên.

Nhìn về tương lai, điều gì cần xảy ra để các phương pháp hình thức chuyển từ việc áp dụng hẹp đến một phần tiêu chuẩn của chu kỳ phát triển phần mềm?

Để một thời gian, tôi biết hai điều cao cấp mà Quint cần cho sự áp dụng nhiều hơn: chi phí thấp hơn và giá trị cao hơn. Tôi nghĩ điều này áp dụng cho nhiều thứ khác nữa. Các phương pháp hình thức vừa nhận được một sự thúc đẩy lớn trong cả hai điều đó, với AI giảm đáng kể chi phí của việc viết các đặc tả hình thức và cũng tạo ra một môi trường thiếu tin cậy và hiểu biết nơi các phương pháp hình thức có thể có tác động và giá trị nhất.

Với AI thay đổi những gì nghề nghiệp của chúng tôi là, ít nhất đến một mức độ nào đó, tôi hy vọng sự thay đổi này là hướng tới các quyết định thiết kế cấp cao hơn và sự chính xác của hành vi, làm cho các phương pháp hình thức trở thành một công cụ hàng ngày; và không phải là chúng tôi không hiểu bất kỳ mã hoặc hệ thống nào nữa và dành tất cả thời gian của mình để xem xét mã được tạo bởi AI mà không có bất kỳ công cụ nào để giúp chúng tôi suy nghĩ về nó.

Cảm ơn bạn vì cuộc phỏng vấn sâu sắc; những người đọc quan tâm đến việc tìm hiểu thêm về ngôn ngữ đặc tả thực thi này để mô hình hóa và xác thực các hệ thống phức tạp, bao gồm cả công cụ và cách bắt đầu, có thể khám phá Quint.