Gabriela Moreira, CEO of Quint di Informal Systems – Seri Wawancara

Gabriela Moreira, CEO of Quint di Informal Systems, adalah insinyur peneliti yang mengkhususkan diri dalam bahasa pemrograman dan metode formal, dengan fokus kuat pada membangun alat yang membuat verifikasi sistem kompleks lebih mudah diakses oleh insinyur. Ia memimpin pengembangan Quint, bahasa spesifikasi eksekusi modern berbasis TLA+, di mana ia terus memelihara dan mengembangkan bahasa dan tooling-nya. Pekerjaannya mencakup verifikasi formal, analisis statis, dan pengembangan alat, dan ia juga telah berkontribusi pada akademisi dengan mengajar metode formal, mencerminkan perpaduan antara praktik rekayasa dan kedalaman teoretis.

Quint, dikembangkan dan dipelihara di Informal Systems, adalah bahasa spesifikasi modern yang dirancang untuk memodelkan, menguji, dan memverifikasi sistem kompleks seperti jaringan terdistribusi, blockchain, dan basis data. Dibangun di atas fondasi Logika Temporal Tindakan (TLA), Quint memperkenalkan sintaksis yang lebih ramah pengguna, serta tooling canggih seperti pengecekan tipe, simulasi, dan verifikasi model, yang memungkinkan insinyur mendeteksi kegagalan sistem sebelum penerapan. Platform ini menekankan spesifikasi yang dapat dijalankan, memungkinkan pengembang tidak hanya untuk mendeskripsikan perilaku sistem tetapi juga untuk mengujinya dan menjelajahinya secara aktif, menjembatani kesenjangan antara kebenaran teoretis dan implementasi dunia nyata.

Kembali ke awal, apa yang pertama kali membangkitkan minat Anda dalam pemrograman, dan bagaimana Anda akhirnya menemukan jalan Anda ke dalam metode formal dan sistem terdistribusi?

Saya adalah seorang penggemar game yang memiliki komputer yang buruk, dan saya menyadari bahwa saya menikmati memperbaiki masalah dan membuatnya berfungsi. Saya mendaftar untuk ilmu komputer dan tertarik pada teori dan compiler. 

Pada 2015, saya diperkenalkan dengan kontes pemrograman. Di dalamnya, Anda biasanya mendapatkan beberapa contoh input dan output yang diharapkan, dan Anda menulis kode yang memecahkan masalah dan berfungsi untuk contoh-contoh tersebut. Namun, setelah Anda mengirimkannya untuk dievaluasi, kode sebenarnya diuji dengan banyak contoh lain di luar yang ditunjukkan kepada Anda. Kesadaran bahwa kode mungkin berfungsi untuk skenario yang saya lihat atau pikirkan, tetapi masih gagal dalam kasus yang belum saya pertimbangkan, membuat pemrograman menjadi tantangan yang saya cintai.

Bekerja di industri, saya dengan cepat tertarik pada sistem terdistribusi, di mana kita harus mempertimbangkan urutan pesan yang berbeda, mode kegagalan yang berbeda, dan dunia perilaku tersembunyi. Pada 2018, seorang rekan kerja memperkenalkan saya dengan bahasa spesifikasi formal yang disebut TLA+. Saya langsung terpesona. Saya segera mulai membangun alat di sekitar TLA+ dan telah bekerja di ruang ini sejak saat itu.

Anda telah membangun karir Anda di sekitar metode formal dan bahasa pemrograman, dari pekerjaan awal Anda pada tooling berbasis Logika Temporal Tindakan (TLA+) hingga memimpin pengembangan Quint di Informal Systems. Apa yang memotivasi Anda untuk fokus pada membuat verifikasi formal lebih mudah diakses, dan bagaimana visi itu membentuk desain Quint?

TLA+ terlalu baik untuk tidak digunakan secara luas di industri. Saya masih cukup junior ketika saya mempelajari tentang hal itu, dan saya bergabung dengan panggilan dengan rekan kerja saya untuk mencoba menemukan solusi bersama, dan saya selalu menemukan skenario di mana solusi kita akan gagal. Namun, saya selalu menjadi garis pertahanan terakhir melawan skenario tersebut dalam sebagian besar kasus. Saya merasa ada cara yang lebih baik, kurang mahal, dan lebih berharga untuk menyelesaikan skenario tersebut. Jadi, saya memulai perjalanan akademis saya menuju itu, yang membawa saya ke Informal Systems dan Quint.

Quint tidak awalnya dirancang sebagai produk. Kami membangunnya karena kebutuhan di Informal Systems. Kami menulis spesifikasi TLA+ untuk sistem yang kami butuhkan untuk dipercaya lebih dari yang kami lakukan, tetapi itu tidak berkembang melampaui kelompok kecil orang karena sintaksis yang terlalu menakutkan dengan terlalu banyak simbol matematika, dan tooling tidak memenuhi harapan dasar orang. Kami menunjukkan rekan kerja dan kolaborator eksternal: “lihatlah hal luar biasa yang saya lakukan”, tetapi mereka tidak bisa membacanya, dan tidak memiliki waktu untuk belajar alat baru.

Pilihan desain di Quint mengikuti langsung dari pengalaman itu. Bahasa ini mudah dibaca dan diingat. Hal pertama yang kami bangun adalah ekstensi VSCode yang menyoroti kesalahan saat Anda mengetik. Ini memiliki tipe dan mode yang berbeda untuk memisahkan lapisan secara eksplisit. Ini memiliki REPL sehingga Anda dapat menjelajahi secara interaktif, dan simulator sehingga Anda dapat mendapatkan umpan balik cepat dan mengulangi. Ini mengekspor jejak ke format JSON standar yang mudah diproses mesin. Ini adalah hal-hal yang sudah diharapkan oleh programmer dan yang kami butuhkan sendiri. Verifikasi di bawahnya adalah logika yang sama dengan TLA+.

Saya terobsesi dengan membuat metode formal lebih mudah diakses, dan mengirimkan alat adalah hal yang menyenangkan, tetapi dampak nyata hanya dirasakan jika tim insinyur sebenarnya menggunakannya. Masih ada kesenjangan antara apa yang alat dapat lakukan dan seberapa berguna mereka terasa bagi pengembang, dan saya bekerja untuk menutup kesenjangan itu.

Bagi pembaca yang tidak terbiasa dengan itu, bagaimana Anda menjelaskan apa itu Quint dan mengapa bahasa spesifikasi baru diperlukan di samping alat seperti TLA+?

Sebagian besar spesifikasi adalah dokumentasi. Anda menulis apa yang harus dilakukan sistem, dan Anda memeriksanya dengan membacanya. Masalahnya adalah dokumentasi salah dengan cara yang tidak dapat dideteksi secara mekanis: nama yang tidak ditentukan, perilaku yang ambigu, asumsi implisit. Anda biasanya menemukannya selama implementasi, atau di produksi.

Spesifikasi Quint adalah sesuatu yang dapat dijalankan. Anda memodelkan sistem sebagai mesin state, mendefinisikan sifat yang harus dipenuhi, dan menjalankan atau memverifikasi model. Jika ada pelanggaran, Anda mendapatkan contoh lawan yang menunjukkan langkah-langkah yang memicunya. Itu mengubah kapan dan seberapa murah Anda menangkap kesalahan desain.

TLA+ selalu bisa melakukan itu. Quint membuatnya praktis untuk insinyur yang tidak sudah ahli dalam logika temporal.

Quint dirancang untuk menjembatani kesenjangan antara metode formal dan rekayasa perangkat lunak sehari-hari. Apa yang menjadi penghalang kegunaan terbesar yang Anda targetkan untuk dihilangkan dibandingkan dengan pendekatan tradisional?

Jujur, penghalang kegunaan terbesar adalah sintaksis. Itulah mengapa kami memulai dengan sintaksis. Setelah mengatasi itu, kami bisa fokus lebih pada faktor lain. Sistem tipe dan efek Quint datang untuk menandai sebanyak mungkin kesalahan sebelum memulai proses verifikasi biasa, dan orang-orang sangat menghargainya. Itu membuat kami menulis spesifikasi yang lebih berkualitas yang bahkan lebih banyak orang bisa baca. Kami mengintegrasikan semua itu dalam editor, dan menawarkan fungsionalitas dasar yang semua pengembang berhak untuk mengharapkannya.

Dampak terbesar setelah itu adalah simulator kami. Itu dimulai sebagai cara untuk menawarkan orang umpan balik pertama tentang perilaku sistem mereka, sebagai pengembang ingin bisa, dengan cara tertentu, menjalankan kode setelah mereka menulisnya. Itu kemudian terbukti sangat berharga sebagai cara untuk mendapatkan kepercayaan pada spesifikasi yang terlalu besar untuk verifikasi menangani, karena keahlian mengadaptasi spesifikasi untuk membuatnya layak untuk verifikasi tidak boleh dianggap enteng. Simulator kami membuat kepercayaan lebih mudah diakses dan kami telah menggunakannya secara luas dalam banyak proyek.

Poin kesulitan terbesar saya dengan sintaksis TLA+ adalah seberapa sering saya mencampurkan garis miring dan garis miring biasa, dan Anda perlu mengetikkan itu banyak. Saya lebih menyukai sintaksis Quint, tetapi apa yang benar-benar membuat saya tidak bisa kembali adalah semua tooling.

Salah satu kekuatan Quint adalah kemampuannya untuk memodelkan dan menguji sistem terdistribusi sebelum penerapan. Bagaimana ini mengubah cara insinyur harus berpikir tentang membangun sistem seperti blockchain atau infrastruktur waktu nyata?

Perubahan terbesar adalah memindahkan validasi lebih awal. Leslie Lamport, pencipta TLA+, membandingkan menulis spesifikasi sebelum kode dengan membuat blueprints sebelum pekerjaan konstruksi. Bahkan jika Anda sudah membangun sesuatu tanpa blueprint, masih merupakan ide yang baik untuk menulisnya sekarang dan menggunakannya untuk menginformasikan perubahan lebih lanjut.

Di industri perangkat lunak, kita menggunakan file markdown dan papan tulis. Mungkin Anda bisa membandingkannya dengan mencoba mendeskripsikan bangunan secara tekstual. Itu berhasil, tetapi apakah Anda tahu apakah ukuran dindingnya sesuai? Quint menawarkan cara untuk mendeskripsikan sistem di mana Anda bisa se tinggi tingkat yang diinginkan, dan mendapatkan wawasan tentang perilakunya dan kebenarannya.

Quint dibangun di atas fondasi TLA+, yang secara luas digunakan untuk mendeskripsikan sistem terdistribusi. Bagaimana Anda menjaga keseimbangan antara mempertahankan keteguhan teoretis tersebut sambil membuat bahasa lebih ramah pengguna?

Keputusan kunci adalah membatasi Quint pada fragmen TLA (logika di balik TLA+) daripada mengekspos semua yang diizinkan oleh logika. TLA sangat ekspresif, dan beberapa ekspresivitas tersebut termasuk operator yang tidak didukung oleh alat apa pun, dan memungkinkan kombinasi yang orang pahami dan gunakan secara salah, membuatnya sangat sulit untuk didebug. Kami membuat keputusan yang disengaja: tetap dengan apa yang sebenarnya dibutuhkan oleh spesifikasi yang realistis, dan hindari apa yang memiliki potensi untuk membingungkan.

Sistem tipe dan efek menambahkan keterbatasan, tetapi keterbatasan yang berguna. Mereka mencegah sejumlah besar kesalahan spesifikasi yang tidak menyenangkan ketika ditemukan setelah verifikasi sudah berjalan. Tipe hampir sepenuhnya diinferensi dan efek disembunyikan dari pengguna, sehingga menambah nilai tanpa gesekan.

Sebelum saya mempelajari tentang keberadaan TLA+, saya melakukan pekerjaan penelitian di sistem tipe, yang berarti bahwa pemeriksa tipe Quint kemungkinan adalah komponen favorit saya untuk ditulis. Saya ingat minum kopi rasa Paçoca di bulan-bulan pertama saya di Informal sambil meninjau beberapa makalah sistem tipe dan berpikir “hidup saya luar biasa”. 

Membuat bahasa yang baik untuk digunakan sambil tetap mempertahankan korespondensi dengan TLA+ (karena spesifikasi Quint dapat diterjemahkan ke TLA+) adalah latihan bahasa pemrograman, dan diskusi dengan tim adalah sumber daya yang paling membantu, diikuti oleh umpan balik dari pengguna awal. Masih ada perbaikan yang kami inginkan, dan mungkin itu adalah bagian favorit saya dari pekerjaan.

Anda juga telah bekerja pada analisis statis dan sistem tipe. Bagaimana pengalaman tersebut mempengaruhi pemeriksaan tipe Quint, tooling, dan pengalaman pengembang secara keseluruhan?

Pelajaran terbesar yang saya pelajari di dunia itu adalah bahwa tidak semua bahasa sama. Anda akan mendengar orang mengatakan bahwa itu hanya masalah belajar sintaksis baru, semua konsep yang sama masih berlaku, sehingga semua bahasa sama dan itu hanya masalah selera. Itu tidak benar. Bidang bahasa pemrograman memiliki peneliti hebat yang melakukan pekerjaan luar biasa untuk memajukan bidang ini, dan itu tidak hanya untuk membuat bahasa terlihat lebih cantik atau lebih sesuai dengan selera mereka.

Pemrograman fungsional diperkenalkan kepada saya sangat awal, saya belajar Haskell pada saat yang sama saya belajar C (bahasa pemrograman pertama saya), dan saya sangat berterima kasih untuk itu. Ini adalah fondasi yang membantu saya melihat bahwa mengisolasi mutasi state dan non-determinisme ke lapisan tipis di Quint, dan memiliki semua kompleksitas dalam fungsi murni secara objektif membantu dalam banyak faktor, dan itu bukan hanya masalah selera. Saya tidak berpikir membangun Quint akan produktif jika masalah selera sering dibahas.

Mengajar metode formal sebagai dosen memberi Anda perspektif unik. Apa yang menjadi kesalahpahaman umum yang dimiliki insinyur tentang verifikasi formal saat ini?

Baik, saya mengajar mahasiswa sarjana yang baru memulai di industri. Sebagian besar dari mereka tidak pernah mendengar tentang metode formal atau verifikasi formal sebelumnya, jadi tidak ada kesalahpahaman! Kurikulum dibuat sehingga sebagian besar dari mereka juga tidak belajar tentang sistem terdistribusi, dan sekitar setengah dari mereka akan belajar tentang thread di semester yang sama. Saya biasanya mengatakan kepada mereka bahwa saya merasa seperti mengajar mereka apa itu payung sebelum mereka mengalami hujan!

Saya lebih termotivasi untuk mengajar mereka bagaimana metode formal dan menspesifikasikan sistem secara formal dapat membantu kita bernalar tentang solusi dan menemukan kasus tepi daripada membuat mereka berpikir bahwa mereka harus memverifikasi formal setiap perangkat lunak yang mereka tulis. Tugas akhir saya adalah setup RPG meja di mana urutan yang berbeda yang pemain bisa ambil dan setup yang berbeda harus dipertimbangkan, mencoba untuk meniru kesulitan yang kita hadapi dalam sistem terdistribusi sebanyak mungkin. Itu berhasil menjadi cukup sulit sehingga mereka harus menggunakan alat untuk menemukan kasus tepi dan meningkatkan solusi mereka untuk mengalahkan monster di akhir. Semoga ketika mereka menghadapi situasi serupa di tempat kerja suatu hari nanti, mereka akan mengingat saya. Beberapa dari mereka sudah melakukannya.

Ada minat yang tumbuh untuk menggabungkan AI dengan pengembangan perangkat lunak. Apakah Anda melihat peran untuk AI dalam membantu pengembang menulis, memvalidasi, atau bahkan menghasilkan spesifikasi formal menggunakan alat seperti Quint?

Peran yang signifikan, dan itu sudah terjadi. Ilmu komputer lebih besar dari menulis kode, dan AI membuka pintu ke cara baru untuk menggunakan metode formal. LLM adalah baik dalam menulis spesifikasi Quint dari deskripsi bahasa alami tentang sistem dan bahkan kode yang ada. Kit LLM Quint memiliki agen Claude Code yang mengambil deskripsi bahasa Inggris tentang protokol dan menghasilkan spesifikasi Quint yang dapat dijalankan dan diperiksa segera.

Pada saat yang sama, Quint juga membantu pengembang mempercayai kode yang ditulis dengan AI. Saya sangat percaya bahwa kepercayaan harus datang dari pemahaman, bukan beberapa centang ajaib. Bekerja pada spesifikasi Quint yang mengarahkan dan memeriksa kode implementasi berarti pengembang masih dapat memiliki dan memahami perilaku sistem, mengatasi utang kognitif yang dapat dibuat oleh penggunaan AI dan menyediakan cara yang lebih tegas untuk memvalidasi kode yang dihasilkan.

Kami menggunakan LLM sebagai alat bahasa yang menulis definisi Quint yang tepat dari niat bahasa alami, dan kemudian memberikan alat Quint kepada AI sehingga dapat melakukan hal-hal yang tidak dapat dilakukan sendiri, seperti menemukan kasus tepi.

Menghadap ke depan, apa yang perlu terjadi agar metode formal berpindah dari adopsi khusus menjadi bagian standar dari siklus hidup pengembangan perangkat lunak?

Untuk beberapa waktu sekarang, saya tahu dua hal yang Quint butuhkan untuk adopsi yang lebih luas: biaya yang lebih rendah dan nilai yang lebih tinggi. Saya pikir ini berlaku untuk banyak hal lain juga. Metode formal baru saja mendapatkan dorongan besar dalam kedua hal itu, dengan AI sangat mengurangi biaya menulis spesifikasi formal dan juga menciptakan lingkungan kurangnya kepercayaan dan pemahaman di mana metode formal dapat paling berdampak dan berharga.

Dengan AI mengubah apa yang menjadi profesi kita, setidaknya sampai batas tertentu, saya berharap perubahan ini menuju desain tingkat yang lebih tinggi dan kebenaran perilaku, membuat metode formal menjadi alat sehari-hari; dan bukan menuju kita tidak memahami kode atau sistem apa pun lagi dan menghabiskan semua waktu kita meninjau kode yang dihasilkan AI tanpa alat untuk membantu kita bernalar tentang hal itu.

Terima kasih atas wawancara yang mendalam; pembaca yang tertarik untuk mempelajari lebih lanjut tentang bahasa spesifikasi eksekusi ini untuk memodelkan dan memverifikasi sistem kompleks, termasuk tooling dan cara memulai, dapat menjelajahi Quint.