Zerdali

Yapay zeka modelleri için yaratılan, yapay zeka modelleri tarafından daha kolay kullanılabilen, bir fonksiyonun ne yaptığını, hangi veriye dokunduğunu imzasında taşıyan, derleyicisi bunu denetleyen bir programlama dili.

fn exists(name: Str@personal) -> Bool@public !{fs.read}

Bu tek satırda çoğu dilin söyleyemediği iki şey var:

• !{fs.read} — bu fonksiyonun yapabileceği efektlerin tam listesi. Bildirmediğin bir efekti yaparsan derlenmiyor.
• @personal → @public — verinin nereye gidebileceği, ve bunun daralabildiği tek nokta: declassify, ve yazılı bir gerekçe istiyor.

Neden var

Efekt sistemi de bilgi akışı da yirmi yıldır biliniyor, ve her biri bir yerlerde uygulanmış durumda — ama hiçbir zaman aynı imzada. Koka, Eff, Frank ve Unison efekti tipe koyuyor; bilgi akışı yok. Jif ve FlowCaml damgayı tipe koyuyor; efekt sistemi yok. OCaml 5'te efekt mekanizması var ama tipin dışında. Haskell'de tek bir IO hem dosya okumayı hem süreç başlatmayı kapsıyor — bir şey oluyor diyor, ne olduğunu değil.

Yani bugün ya bir fonksiyonun diske uzandığını bilebiliyorsun, ya bir değerin kişisel veri olduğunu. İkisini birden tek imzadan değil.

Zerdali bu boşluk için var. İki soru aslında tek soru: bu kod neye uzanabilir, ve içinden dışarı ne çıkabilir?

Bunun getirdikleri

• zerdali audit — koşmadan önce okunabilen bir yetki raporu: her fonksiyonun efektleri, her damganın eriştiği yer, her daraltma gerekçesiyle.
• zerdali test — testler hiçbir yetki verilmeden koşuyor. Gerçek diske uzanan test düşer; dosyaya ihtiyacı olan test onu dilin içinde karşılar. Sahte (mock) çerçevesi yok, çünkü gerekmiyor.
• Sonlanma ya yapısal olarak kanıtlanıyor ya da imzada !{div.loop} olarak yazılıyor. Burada "saf", "yan etkisiz ve sonlanır" demek.

Kimin için

Kişisel veriye dokunan, ne yaptığı denetlenebilir olması gereken programlar yazan geliştiriciler için — ve dili kısa bir belgeden öğrenip doğru yazması beklenen LLM'ler ve ajanlar için. İkinci hedef iddia olarak bırakılmadı, ölçüldü: üç satıcıdan on üç model, 2.7k simgelik tek bir dil kartıyla.

Ne kurulur, ne çalışır

Dağıtılan şey derlenmiş bir ikili: zdc. Statik bir ELF — sanal makine yok, yorumlayıcı yok, libc bile yok. Kurup çalıştırmak için makinede hiçbir şeyin bulunması gerekmiyor, ve derlediği programlar da aynı şekilde tek başına koşuyor. Çalışma zamanı diye bir katman yok.

Derleyici kendi kodunu doğrudan üretiyor: kendi x86-64 kodlayıcısı ve kendi ELF yazıcısı var. Arada assembler yok, linker yok.

Doğruluk nasıl ölçülüyor

Bir dilin tek uygulaması varsa, o uygulamanın davranışı dilin tanımı olur — hatası da tanımın parçası olur, çünkü onu yanlışlayacak bir şey yoktur. Bu projede iki ölçüt var, ve ikisi de iddia değil, her değişiklikte koşan birer ölçüm:

Bağımsız ikinci bir uygulama. Aynı programda aynı belirteçleri, aynı imzaları, aynı tanıları, aynı ara kodu ve aynı baytları üretmek zorundalar; ayrıldıkları her nokta bir hatadır. İkisi de on altı komutun hepsini cevaplıyor (check, run, build, test, audit, doc, fmt, fix, holes, debug, explain, spec, search, serve, lsp, pkg) ve bir kural değişikliği ikisine birden iniyor. Bu ölçüt uygulama ayrı bir dilde yazıldı, çünkü kâhin denetlediği şeyden bağımsız olmalı: aynı dilde yazılsaydı ikisi aynı yanlış varsayımı paylaşabilir ve karşılaştırma hiçbir şey görmezdi.

Sabit nokta. zdc kendi kaynağını derlediğinde ortaya kendisiyle bayt bayt aynı bir ikili çıkıyor. Bu bir özellik değil, bir kanıt: kod üretiminin, denetleyicinin ve bağlayıcının bir milyon dokuz yüz bin baytın tamamında aynı kararı iki kez verdiği anlamına geliyor. Tek bir bayt kaysa ölçüm düşer.

Denetleyicinin yaptığı

• Efekt satırı — çıkarımla değil, imzayla. Bir efekt ya imzada bildirilir ya da bir tutucuda (handle) karşılanır. Karşılandığında imzadan düşüyor.
• Bilgi akışı — damgalar tipin parçası. nameden türeyen her şey kişisel kalıyor, karşılaştırma bile (hangi dalın seçildiği de bir bilgi).
• Sonlanma — dilde döngü yok; her yineleme özyinelemeyle. Bir çağrı döngüsüne katılan her fonksiyon !{div.loop} bildirmek zorunda, özyineleme yapısal olarak küçülmedikçe. Kanıt bilinçli olarak basit tutuldu: n - 1 insan gözüyle küçülüyor ama denetleyici onu aramıyor — kanıtın okunabilir kalması, kanıtlanan kümenin büyümesinden değerli sayıldı.
• Sahiplik — own Buf kopya yerine yerinde yazma yapıyor. İmzada yazılı, çıkarılmıyor: çıkarım iki uygulamada da aynı cevabı vermek zorunda kalırdı, yani dilin tanımının parçası olurdu.

Arka uç

Yerel x86-64 kod üretimi, kendi ELF yazıcısı ve kendi çalışma zamanı. buf_dot gibi çekirdekler SSE2 ile vektörleşmiş. Dış bağımlılık yok, derleme sonrası çalışma zamanı yok.

LLM'ler için

LLM.md — yaklaşık 2.7k simge, ve dilin tamamı. Ölçümde modele bundan başka bir şey verilmiyor; gönderdiği program derlenip koşuluyor, yeşil değilse geri dönen tek şey derleyicinin kendi tanısı oluyor. Her hata çiğnediği kuralı taşıyor ve yapabildiğinde yazılacak satırı söylüyor.

Dürüst durum: bu dil kendine karşı çok iyi sınanmış, başka hiç kimse tarafından sınanmamış.

• Bağımsız inceleme yok. Kendi geliştirmesi dışında kullanıcısı da yok.
• Differential'ın söylediği şey sınırlı. İki uygulamanın aynı olduğunu söylüyor, doğru olduğunu değil. Bu projede bulmaya değer her hata, korpusta onu koşturan bir program olmadığı için görünmezdi — ve o programı yazana kadar görünmez kaldı.
• Yığın taşması bir tanı değil, bir çökme. Sonsuz özyinelemeye giren bir program 8 MB'lık yığını tüketip segfault veriyor. Dil bunu bildirmeyi zaten şart koşuyor (!{div.loop}), ama bildirilmiş bir ıraksama koşulduğunda söylediği şey yalnızca "sinyal 11" oluyor.
• Platform: yalnız Linux x86-64. Başka mimari, başka işletim sistemi yok.
• Bellek tavanı: derleyici kendini derlerken yaklaşık 8 GB istiyor.
• Ekosistem yok. Paket yöneticisi (zdc pkg) var ama paket kaydı yok; standart kütüphane küçük.
• Dil küçük tutuldu. Adsız fonksiyon yok, tek yönlü sonlanma kanıtı, tek sahipli tampon dönüşü gibi bilinçli sınırlar var. Bunlar eksik değil karar; hangisinin hangisi olduğu V1.mdde yazılı.

Kataloğa yazılan ölçümler ekip beyanıdır; buradakiler de öyle — ama hepsi depoda duran ve tekrar koşturulabilen betiklerden geliyor.