TScert, Lean ile doğrulanmış bir denetleyiciyle TypeScript fonksiyonlarını tip güvenli kanıtlıyor

cristianoc hesabı altında GitHub'da yayımlanan ve Hacker News'in ana sayfasında öne çıkan TScert adlı araştırma projesi, TypeScript tip denetleyicisindeki sağlamlık (soundness) boşluklarını hedef alıyor. Yaklaşımı alışılmadık: bir TypeScript fonksiyonu yalnızca tip güvenli olduğunu makine tarafından doğrulanmış bir kanıt taşıdığında kabul ediliyor ve bu kanıtları geçerli kılan küçük denetleyicinin kendisi de Lean proof assistant içinde sağlam olduğu kanıtlanmış durumda.

TScert ne yapıyor

TypeScript'in tip sistemi bazı noktalarda bilinçli olarak sağlam değil. Projenin README'sinde açıklandığı gibi, any, tip iddiaları (assertion), denetlenmeyen indeksli okumalar ve kovaryant diziler gibi özellikler programların tsc'den sorunsuz geçmesini sağlarken, tipin string vaat ettiği yerde yine de undefined okunmasına izin verebiliyor. TScert, kabul ettiği kod için daha katı bir anlaşma sunuyor: bir fonksiyonun tip bildirimlerini karşılayan her girdi için, fonksiyonun resmi bir modele çevrilmiş hâli yanlış biçimdeki bir değere asla bir işlem uygulamayacak ve bildirilen sonuç tipinin dışında bir değer asla döndürmeyecek. Bu garantiyi Lean'da bir teorem ifade ediyor ve teorem, kabul kararını veren denetleyicinin kendisini de kapsıyor.

README'deki örnek, bir dizinin uzunluğunu alıyor, son elemanı çıkarıyor, sonra eski uzunluk eksi bir indeksiyle elemana erişiyor. noUncheckedIndexedAccess'ın kapalı olduğu strict modunda tsc, fonksiyonu string sonuç tipiyle kabul ediyor; oysa fonksiyon çalışma zamanında undefined döndürüyor. TScert bunu reddediyor ve indeks ifadesinin elindeki iddianın undefined | string olduğunu, dönüş sözleşmesinin ise string talep ettiğini bildiriyor. Sonuç tipi string | undefined olarak yeniden yazıldığında aynı fonksiyon kabul ediliyor.

Güvenilmeyen öneriler, tek doğrulanmış denetleyici

Ardışık düzen (pipeline), neredeyse hiçbir şeye güvenilmeyecek şekilde tasarlanmış. TypeScript'in compiler API'si üzerine kurulu bir ön yüz kaynağı ve bildirimleri okuyor; yürütmeyi Lean planlıyor. Producer adlı OCaml bileşeni her ifade ve değişken için bir tip öneriyor, ama bu yanıtlar olgu değil iddia olarak ele alınıyor. Lean, fonksiyonu önerilen tiplerle kullanarak küçük bir resmi dile — calculus — çeviriyor; bu dilin yürütme ve güvenlik anlamları Lean'ın kendisinde tanımlı. Güvenilmeyen bir arama son olarak bir certificate, yani çevrilmiş programın tiplerine uyduğunu gösteren bir türetme öneriyor ve doğrulanmış denetleyici bu sertifikayı aynı çeviriye karşı geçerli kılıyor.

Kabul neyi garanti ediyor — neyi garantilemiyor

README'ye göre kabul, fonksiyonun çevirisinin, bildirilen tiplerle uyumlu girdiler ve heap üzerinde çalıştırıldığında takılmadığını ve sonuç tipinin dışında bir değer döndürmediğini kanıtlıyor. Fonksiyon yine de exception fırlatabilir ya da sonsuza kadar çalışabilir. Güven tabanı açıkça belirtilmiş: TypeScript'ten calculus'a çeviri gözden geçirildi ve test edildi ama kanıtlanmadı; kütüphane ve host fonksiyonlarının gözden geçirilmiş sözleşmelere uyduğu varsayılıyor; çağıranların ve import edilenlerin bildirilen tipleri karşıladığı varsayılıyor; ve Lean'a güveniliyor.

Durum ve kapsam

TScert bir ürün değil, açık uçlu bir araştırma çabası. Kıyaslaması kendi ön yüzü: ae20a6c6 commit'ine bağlı ve 2026-11-04 tarihli bir sayıma göre, sürüm 0.94'te deponun tools/ dizinindeki 686 fonksiyondan 643'ü, her biri kendi biriminde denetlenmek üzere doğrulanıyor.

Desteklenen alt küme yine de geniş: değişkenler, pattern'lar, koşullar, switch, döngüler (for...of ve for...in dahil), etiketli bloklar ve try/catch/finally; literal tipli primitive'ler, aritmetik, karşılaştırmalar, template literal'ler, typeof, in, instanceof ve katı eşitlik; spread'li nesne literal'leri, record'lar, index signature'lar, diziler, tuple'lar, optional chaining, enum'lar; alan, metod ve inheritance içinden sınıflar; opsiyonel, varsayılan ve rest parametreli closure'lar, izin verilen her tip argümanı için denetlenen generic fonksiyonlar ve native promise üzerinden async/await; ayrıca alias'lar, interface'ler, union'lar, intersection'lar ve gözden geçirilmiş sözleşmelerle kütüphane tipleri. any tamamen reddediliyor, e as T gibi iddialar hiçbir şey kanıtlamıyor ve desteklenmeyen biçimler bir gerekçe ve konumla birlikte reddediliyor. Projeyi derlemek için Node, sabitlenmiş bir Lean toolchain'i, OCaml ve Dune gerekiyor.

Temeller ve alışılmadık bir lisans

Depo, uzun bir araştırma soyuna atıf yapıyor — Appel ve McAllester'ın temel proof-carrying-code modeli, Ahmed'ın değiştirilebilir durum için tip anlamları üzerine çalışması, Wright ve Felleisen'ın sözdizimsel tip sağlamlığı, Reynolds'ün parametrisitesi, Abadi ve Cardelli'nin nesne kuramı, semantik altipleme, JSCert, ECMAScript belirtimi ve Lean 4.

Lisansı, mimarisi kadar ayırt edici. Proje, NON-AI MIT License adını verdiği bir lisans kullanıyor: MIT koşulları, artı kodun makine öğrenimi sistemlerini eğitmek veya geliştirmek amacıyla ve bu amaçla kurulmuş veri kümelerinde kullanımının dışlanması; bu, türevlere de uzanıyor. Ayrıca 2019/790 sayılı (AB) Direktifi'nin 4(3). maddesi kapsamında metin ve veri madenciliğine karşı haklar saklı tutuluyor ve bu, makine tarafından okunabilir bir ai.txt dosyasında yeniden ifade ediliyor.

Neden önemli

TypeScript en yaygın kullanılan tipli diller arasında ve sağlamlık boşlukları, beklenmedik bir undefined'in peşine düşmüş herkese tanıdık. TScert'in önemi mevcut kapsamından çok mimarisinde yatıyor: çevredeki araç zincirinin çıkarsadığı hiçbir şeye güvenilmiyor, her tip iddiası ve certificate, sağlamlığı bir teorem olan küçük bir doğrulayıcıdan geçiyor ve parça sınırı dürüst — kanıtlanamayan ne varsa bir açıklamayla reddediliyor. Bu, proof-carrying-code fikrinin yaygın bir endüstriyel dile uygulanmış hâli. Yaklaşım kendi kıyaslamasının ötesine ölçeklenirse, kritik kod yollarında fonksiyon başına makine tarafından doğrulanmış garantiler için pratik bir yola işaret ediyor — tsc'nin tamamlayıcısı, yerine geçeni değil.