Ide & Wawasan

Mengeksplorasi pengembangan AI-first, coding guardrail, dan arsitektur untuk dibuang.

model-checkingllmrustformal-proofs

LLM dapat menghasilkan kode Rust. Pembuktian formal adalah masalah yang sama sekali berbeda.

Model bahasa besar menulis kode Rust yang menakjubkan baiknya, tetapi ketika Anda meminta pembuktian formal, mereka menghasilkan invarian yang tidak ada dan menciptakan sintaks yang tidak diterima oleh verifikator apa pun. Berikut ini yang benar-benar mereka lakukan dengan benar, di mana mereka gagal, dan bagaimana menggunakannya meskipun begitu.

LLM dapat menulis Rust yang dikompilasi dan bahkan lulus . Apa yang tidak dapat mereka lakukan secara andal adalah menulis pembuktian formal bahwa kode…
model-checkingtemporal-logicformal-methodsverification

Anda Dapat Melakukan Model Checking pada Kode Tanpa Mempelajari Temporal Logic

Bounded model checker seperti Kani dan relational model finder seperti Alloy memungkinkan Anda memverifikasi properti dengan assertion dan constraint biasa. Anda mengorbankan pembuktian liveness untuk kurva pembelajaran yang diukur dalam jam, bukan minggu.

Anda tidak perlu mempelajari logika temporal linear untuk menggunakan model checker. Alat seperti Kani, CBMC, dan Alloy memungkinkan Anda memverifikasi…
model-checkingrustverificationformal-methods

Anda dapat membuktikan kode Rust benar tanpa menulis satu pun bukti, tapi ruang keadaan adalah tagihannya

Alat model checking seperti Kani memungkinkan Anda memverifikasi properti Rust dengan assertion alih-alih bukti formal. Masalahnya adalah apa yang terjadi ketika loop Anda tidak memiliki batas kecil.

Anda dapat membuktikan kode Rust benar tanpa menulis satu pun bukti. Alat yang melakukannya disebut model checker, dan untuk Rust yang paling praktis saat ini…
model-checkingdistributed-systemstlaplusprotocol-design

Anda Tidak Bisa Melakukan Unit Test pada Protokol Terdistribusi, tetapi Anda Bisa Melakukan Model Checking

Bug terdistribusi mahal untuk diperbaiki setelah deployment. Model checking memungkinkan Anda menemukannya sebelum menulis satu baris kode implementasi pun. Berikut cara melakukannya dengan TLA+.

Anda tidak bisa melakukan unit test pada protocol terdistribusi. Unit test menjalankan satu proses di satu mesin dalam satu urutan. Protocol Anda menjalankan…
dsls-bounded-contextllmconstrained-generationgrammar

Grammar-constrained decoding: memaksa LLM mengeluarkan sintaks yang valid di setiap token

LLM menghasilkan sintaks yang salah karena mereka melakukan sampling token secara probabilistik. Grammar-constrained decoding menyaring kosakata di setiap langkah sehingga hanya token yang mempertahankan validitas sintaksis yang dikeluarkan.

Minta LLM untuk menghasilkan objek JSON dan pada akhirnya ia akan mengeluarkan trailing comma, newline yang tidak di-escape di dalam string, atau bare word di…
dsls-bounded-contextdesign-systemsllmthemes

Menerjemahkan dari Bahasa Inggris ke tema itu mudah. Menjadikannya deterministik adalah masalah sesungguhnya.

Anda dapat menghasilkan design token dari deskripsi Bahasa Inggris sederhana, tetapi hanya jika Anda memperlakukan deskripsi tersebut sebagai DSL konteks terbatas dengan kontrak schema dan snapshot test.

Ya, Anda dapat mendeskripsikan sebuah tema dalam Bahasa Inggris dan mendapatkan design system yang berfungsi. Masalahnya adalah deskripsi dalam Bahasa Inggris…
dsls-bounded-contextdslparser-combinatorstypescript

Buang file grammar: tulis parser DSL-mu dengan TypeScript biasa

Parser generator terlalu berlebihan untuk sebagian besar DSL bounded-context. Parser combinator memungkinkanmu membangun parser yang berfungsi dalam bahasa yang sama dengan aplikasimu, tanpa kode yang dihasilkan dan tanpa langkah build.

Jika pernah kamu membuka file grammar Yacc dan bertanya-tanya mengapa membangun bahasa memerlukan belajar bahasa kedua, kamu tidak sendirian. Parser generator…