Martin Kleppmann, yapay zekanın yazılım geliştirmedeki etkilerine dair yeni bir bakış açısı sunuyor: Yapay zekanın, onlarca yıldır niş bir alan olan resmi doğrulamayı (formal verification) yazılım mühendisliğinin ana akımına taşıyacağına inanıyor. Rocq, Isabelle, Lean gibi ispat yardımcıları ve ispat odaklı programlama dilleri, bir kod parçasının belirli bir spesifikasyonu karşıladığını matematiksel olarak kanıtlamayı mümkün kılıyor. Bu araçlar, işletim sistemi çekirdekleri ve C derleyicileri gibi büyük, resmi olarak doğrulanmış yazılım sistemlerinin geliştirilmesinde kullanılmış olsa da, şu anda genellikle araştırma projeleriyle sınırlı kalıyor.
Resmi doğrulamanın yaygınlaşamamasının temel nedeni, ispat yazma sürecinin hem son derece zor (doktora seviyesinde eğitim gerektiren) hem de çok zahmetli olmasıdır. Örneğin, seL4 mikro çekirdeğinin 8.700 satırlık C kodunu doğrulamak için 20 kişi-yıl ve 200.000 satır Isabelle kodu gerektiği belirtiliyor. Bu durum, çoğu sistem için hataların beklenen maliyetinin, bu hataları ortadan kaldıracak ispat tekniklerini kullanmanın beklenen maliyetinden daha düşük olduğu anlamına geliyor. Dünya genelinde bu tür ispatları yazabilecek uzman sayısı da oldukça sınırlı.
Ancak bu durum, büyük dil modellerine (LLM) dayalı kodlama asistanlarının ortaya çıkmasıyla değişmeye başladı. Bu asistanlar, sadece uygulama kodu yazmada değil, aynı zamanda çeşitli dillerde ispat betikleri yazmada da oldukça başarılı hale geliyor. Şu anda uzman bir insan rehberliği gerekse de, bu sürecin önümüzdeki birkaç yıl içinde tamamen otomatikleşeceği öngörülüyor. Resmi doğrulama maliyetlerinin önemli ölçüde düşmesi, çok daha fazla yazılımın doğrulanabilmesini sağlayacak. Dahası, yapay zeka tarafından üretilen kodların insanlar tarafından incelenmesi yerine, yapay zekanın kendi ürettiği kodun doğruluğunu kanıtlaması, yazılım güvenilirliği ve geliştirme süreçlerinde devrim yaratacak.
Yapay zeka, yazılımda hata ayıklamanın maliyetini düşürerek resmi doğrulamayı endüstri standardı haline getirecek ve yazılım güvenilirliğini artıracak.