Gabriela Moreira, CEO of Quint at Informal Systems – Interview Series

Gabriela Moreira, CEO of Quint at 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, sebuah bahasa spesifikasi eksekutable modern berbasis TLA+, di mana ia terus memelihara dan mengembangkan bahasa dan tooling-nya. Pekerjaannya mencakup verifikasi formal, analisis statis, dan tooling pengembang, dan ia juga telah berkontribusi pada dunia akademis dengan mengajar metode formal, mencerminkan perpaduan antara keahlian teknik praktis 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 dari Tindakan (TLA), Quint memperkenalkan sintaks yang lebih ramah pengembang, bersama dengan tooling canggih seperti pengecekan tipe, simulasi, dan verifikasi model, yang memungkinkan insinyur untuk mendeteksi kegagalan sistem sebelum penerapan. Platform ini menekankan spesifikasi eksekutable, yang memungkinkan pengembang untuk tidak hanya mendeskripsikan perilaku sistem tetapi juga menguji dan mengeksplorasi 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 metode formal dan sistem terdistribusi?

Saya adalah seorang penggemar game dengan 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 sana, 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 mereka tunjukkan 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 kepada bahasa spesifikasi formal yang disebut TLA+. Saya langsung terkesan. 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 dari 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 belajar tentangnya, dan saya akan 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 pikir ada cara yang lebih baik, kurang mahal, lebih berharga untuk memecahkan skenario tersebut. Jadi, ide menggunakan metode formal untuk membuat spesifikasi sebelum mengimplementasikan kode diciptakan. Jadi, saya memulai perjalanan akademis saya ke arah itu, yang membawa saya ke Informal Systems dan Quint.

Quint awalnya tidak 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 meluas di luar kelompok kecil orang karena sintaksnya terlalu menakutkan dengan terlalu banyak simbol matematika, dan tooling tidak memenuhi harapan dasar orang. Kami akan menunjukkan kepada rekan dan kolaborator eksternal: “lihatlah hal luar biasa ini 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 mengeksplorasi secara interaktif, dan simulator sehingga Anda dapat mendapatkan umpan balik cepat dan mengulangi. Ini mengekspor jejak ke format JSON standar yang mudah dibaca mesin. Ini adalah hal-hal yang sudah diharapkan programmer dari alat mereka dan yang kami butuhkan sendiri. Verifikasi di bawahnya adalah logika yang sama dengan TLA+.

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

Bagi pembaca yang tidak familiar dengannya, 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 seharusnya 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 properti yang seharusnya dipenuhi, dan menjalankan atau memverifikasi model. Jika ada pelanggaran, Anda mendapatkan contoh counter yang menunjukkan urutan langkah yang memicu itu. Itu mengubah kapan dan seberapa murah Anda menangkap kesalahan desain.

TLA+ selalu bisa melakukan ini. 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 sintaks. Itulah mengapa kami memulai dengan sintaks. Setelah mengatasi itu, kami bisa fokus lebih pada faktor lain. Sistem tipe dan efek Quint menambahkan keterbatasan, tetapi keterbatasan yang berguna. Mereka mencegah kelas kesalahan spesifikasi yang tidak menyenangkan ketika ditemukan setelah verifikasi sudah berjalan. Tipe hampir seluruhnya diinferensi dan efek disembunyikan dari pengguna, sehingga menambah nilai tanpa gesekan.

Setelah itu, simulator kami memiliki dampak terbesar. Ini dimulai sebagai cara untuk menawarkan umpan balik awal tentang perilaku sistem, sebagai pengembang yang ingin menjalankan kode setelah mereka menulisnya. Ini kemudian terbukti sangat berharga sebagai cara untuk mendapatkan kepercayaan pada spesifikasi yang terlalu besar untuk verifikasi, karena keahlian mengadaptasi spesifikasi untuk membuatnya layak untuk verifikasi tidak boleh dianggap remeh. Simulator kami membuat kepercayaan lebih mudah diakses dan kami telah menggunakannya secara ekstensif dalam banyak proyek.

Poin kesalahan terbesar saya dengan sintaks TLA+ adalah seberapa sering saya mencampur garis miring dan garis miring biasa, dan Anda perlu mengetikkan itu banyak. Saya lebih suka sintaks Quint, tetapi apa yang benar-benar membuatnya mustahil untuk kembali adalah semua tooling.

Salah satu kekuatan Quint adalah kemampuannya untuk memodelkan dan menguji sistem terdistribusi sebelum penerapan. Bagaimana ini mengubah cara insinyur harus memikirkan 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 menggambar blueprint 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, kami menggunakan file markdown dan papan tulis. Mungkin Anda bisa membandingkannya dengan mencoba mendeskripsikan bangunan secara tekstual. Ini berhasil, tetapi apakah Anda tahu apakah ukuran dindingnya sesuai? Quint menawarkan cara untuk mendeskripsikan sistem di mana Anda dapat se tinggi level yang diinginkan, dan mendapatkan wawasan tentang perilakunya dan kebenarannya.

Quint membangun di atas fondasi TLA+, yang secara luas digunakan untuk mendeskripsikan sistem terdistribusi. Bagaimana Anda menyeimbangkan mempertahankan ketegaran teoretis sambil membuat bahasa lebih ramah pengembang?

Keputusan kunci adalah membatasi Quint pada fragmen TLA (logika di balik TLA+) daripada mengekspos semua yang diizinkan logika. TLA sangat ekspresif, dan beberapa ekspresivitas tersebut termasuk operator yang tidak didukung oleh alat mana 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 kelas kesalahan spesifikasi yang tidak menyenangkan ketika ditemukan setelah verifikasi sudah berjalan. Tipe hampir seluruhnya diinferensi dan efek disembunyikan dari pengguna, sehingga menambah nilai tanpa gesekan.

Sebelum saya belajar tentang keberadaan TLA+, saya melakukan penelitian di sistem tipe, yang berarti bahwa pengecekan tipe Quint adalah komponen favorit saya untuk ditulis. Saya ingat minum kopi rasa Paçoca di beberapa bulan pertama saya di Informal sambil meninjau beberapa kertas 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 paling berguna, diikuti oleh umpan balik dari pengguna awal. Masih ada perbaikan yang kami ingin lakukan, dan mungkin itu adalah bagian favorit saya dari pekerjaan.

Anda juga telah bekerja pada analisis statis dan sistem tipe. Bagaimana pengalaman tersebut mempengaruhi pengecekan 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 sintaks baru, konsep yang sama masih berlaku, jadi 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.

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 tidak 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 kesalahpahaman yang paling 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 formal dapat membantu kita bernalar tentang solusi dan menemukan kasus tepi daripada membuat mereka berpikir bahwa mereka harus memverifikasi formal semua perangkat lunak yang mereka tulis. Tugas akhir saya adalah setup RPG meja di mana urutan yang diambil pemain dan setup yang berbeda harus dipertimbangkan, mencoba meniru kesulitan yang kita hadapi dalam sistem terdistribusi sebanyak mungkin. Ini 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?

Yang signifikan, dan itu sudah terjadi. Ilmu Komputer lebih besar dari menulis kode, dan AI membuka pintu untuk cara baru menggunakan metode formal. LLM adalah baik dalam menulis spesifikasi Quint dari deskripsi bahasa alami dari sistem dan bahkan kode yang ada. Kit LLM Quint memiliki agen Claude Code yang mengambil deskripsi bahasa Inggris dari 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 perlu 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 memanfaatkan LLM sebagai alat bahasa yang menulis definisi Quint yang presisi 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 tingkat tinggi 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 kekurangan kepercayaan dan pemahaman di mana metode formal dapat memiliki dampak dan nilai terbesar.

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

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