Web3'ün güvenilir olması için gerçekten ne gerekiyor?

Geçen hafta @HeliosStaking podcast'inin bölümünde @RosuGrigore, doğrulanabilirlik, formal yöntemler ve merkeziyetsiz altyapının geleceği için kanıtlanabilir sistemler üzerine konuştu.

↓ İşte öne çıkanlar:

NASA'dan blockchain altyapısına: @RosuGrigore, NASA'daki görev kritik sistemlere formal yöntemler uygulayarak başladı. Bugün, aynı araçlar, kanıtlanabilir doğruluk gerektiren blockchain'lere uygulanıyor.

Runtime Verification nasıl şekillendi: @RosuGrigore, formal yöntemleri gerçek dünya sistemlerine getirmek için @rv_inc'yi kurdu. Başlangıçta hem test hem de formal yöntem konferanslarından reddedildi, “runtime verification” terimi yaklaşımı yeniden tanımladı—runtime gözlem ile doğruluk garantilerini harmanlayarak. Artık bu, sistem güvence kategorisinin tamamını tanımlıyor.

Semantik neden önemli: Formal semantik olmadan, programlama dilleri hareketli hedefler haline gelir. Pi Squared, K Framework ve Matching Logic kullanarak program davranışını matematiksel kesinlikle tanımlayıp nedenler.

@IOHK_Charles ve @VitalikButerin'den destek: IOHK, K dilinde formal dillerin ilk çalışmalarını finanse etti. Vitalik, Ethereum’un Casper protokolü, Vyper, Uniswap ve ETH2 depo kontratını doğrulama çalışmalarına hibe sağladı—bu, alandaki ilk formal doğrulama girişimlerinden bazıları.

Sıralama olmadan doğrulanabilirlik: Pi Squared, claim'lerin—rollup'lar, AI ajanları veya borsalardan—bağımsız ve paralel olarak doğrulanabildiği merkeziyetsiz bir settlement layer tanıtıyor. Global sıralama gerekmez. Sadece kanıt.

“Doğrulanabilirlik olmadan, Web3 olmaz.”

Doğruluk taşınabilir hale gelir.
Gerçeklik programlanabilir olur.