RealWorld Uygulamasını Lean 4 ile Geliştirdim

Özet (Abstract)#

Resmi test paketlerine sahip referans tam yığın (full-stack) uygulaması olan RealWorld, tamamen Lean 4 kullanılarak sıfırdan inşa edildi. Peki bu yapılabilir mi? Evet. Üretim (production) ortamı için hazır mı? Kısmen. Yapısı gereği tamamen hatasız (correct by construction) hale getirilebilir mi? Bir noktaya kadar. Yine de ortalama bir tam yığın uygulamadan çok daha sağlam ve güvenilir hale getirilebileceği kesin. Yazılım öğrenenler için bu çalışma, akademik teorem kanıtlama araçlarının pratik mühendislik dünyasına nasıl adım attığını gösteren harika bir örnektir.

1 Giriş (Introduction)#

Lean 4, Haskell ve OCaml ile aynı aileden gelen fonksiyonel bir programlama dilidir. Çoğu geliştirici onu bir kanıt asistanı (proof assistant) olarak tanır. Ancak son zamanlarda standart kütüphanesine bir HTTP sunucusu eklendi. Topluluk ayrıca Postgres sürücüleri, kriptografi ve HTML oluşturma (rendering) gibi sıradan uygulamaların ihtiyaç duyduğu diğer kütüphaneleri de aktif olarak geliştiriyor.

Peki Lean ile gerçek bir web uygulaması yapılabilir mi? Bunu görmek için bir Medium klonu olan ve hem API hem de web sitesi için resmi test paketleriyle gelen RealWorld uygulamasını geliştirdim. Etkileşim için datastar-lean kullanan önyüz (frontend) dahil olmak üzere, uygulamanın tamamı Lean ile yazıldı.

Bu yazı bir matematik makalesi yapısında kurgulandı; çünkü bu yaklaşım hem eğlenceli hem de mimari yapıyı net tutuyor. İçeriğin büyük kısmı herhangi bir dilde yapacağınız klasik yazılım mühendisliğidir. Gerçekten kanıtlanan kısımlar ise önerme olarak işaretlenmiştir ve Lean, kod her derlendiğinde bu kanıtları otomatik olarak doğrular. Geliştiriciler için buradaki en önemli pratik çıkarım, derleme zamanı doğrulamasının çalışma zamanı hatalarını nasıl en aza indirdiğidir.

2 Varlık (Existence)#

İlk temel soru, Lean dilinde bir RealWorld uygulamasının yazılıp yazılamayacağıdır. Resmi test paketleri bu soruyu somut olarak kontrol edebileceğimiz bir probleme dönüştürür.

Tanım 1 (Definition 1): Bir RealWorld uygulaması, RealWorld'ün hem API test paketini hem de web sitesi test paketini başarıyla geçen bir programdır.

Teorem 1 (Theorem 1): Lean dilinde bir RealWorld uygulaması vardır.

Bunun kanıtı, doğrudan çalışan bir uygulama inşa etmektir. Test paketleri uygulamanın ne yapması gerektiğini tanımlar: API testleri HTTP istekleri gönderip dönen JSON yanıtlarını kontrol eder (bir sunucu gerekir), verilerin istekler arasında korunması gerekir (bir veritabanı gerekir) ve web sitesi testleri gerçek bir tarayıcıda sayfalar arası gezinir (sunucunun sayfa oluşturması gerekir).

İnşa 1 - Sunucu (Construction 1 - The server): Lean'in standart kütüphanesi nisan ayından beri düşük seviyeli bağlantı yönetimini üstlenen Std.Http sunucusuna sahiptir. Bunun üzerine, API rotalarını tip güvenli parametrelerle bir tabloda tanımlamak için lean-routing kullanılmıştır. Örneğin deleteComment işleyicisi (handler), requireUser ile kullanıcının giriş jetonunu kontrol eder, yorumu silmek için servis katmanını çağırır ve 204 No Content yanıtı döner. Web sitesi de aynı servis katmanını çağırdığı için birebir aynı iş kurallarını takip eder. Pratik açıdan bu, iş mantığını tek bir servis katmanında toplamanın kod tekrarını ve tutarsızlıkları önlediğini gösterir.

Diğer tüm temel ihtiyaçlar, her modern programlama dilinde olduğu gibi ekosistemdeki kütüphanelerden karşılanır:

• JSON işlemleri için lean-json
• OpenSSL'in scrypt algoritmasıyla parolaları özetlemek (hashing) için lean-libcrypto
• Giriş jetonları (JSON Web Tokens - JWT) için lean-jose
• CORS, çerezler (cookies) ve statik dosyalar için lean-middleware

İnşa 2 - Veritabanı (Construction 2 - The database): Uygulama verileri Postgres üzerinde tutulur. Postgres'in C istemcisini saran ve bir bağlantı havuzu (connection pool) yöneten leanpostgres kütüphanesi aracılığıyla veritabanı ile iletişim kurulur; böylece SQL sorgularını doğrudan kodun içinde güvenle yazabilirsiniz.