Formal Yöntemler ve Yazılım İnşası

20 yıl önce programların doğruluğunu kanıtlamak için formal teknikler kullanımı son derece aktif bir araştırma konusuydu. Bununla birlikte, o zamanların yöntemleri (ve donanımları) bu tekniklerin yaygınlaşmasını engelledi. Sonuç olarak Bilgisayar Bilimi programlarında az ya da çok ihmal edildiler. Bu çok yazık, çünkü geliştirilen teknikler geniş-ölçekli sistemlerde ve bu sistemlerin güvenilirliğini ciddi bir şekilde katkı sağlama konusunda kullanılabilirler. Bu duruma bir örnek İngiltere'deki yer-merkezli hava trafik kontrol sisteminin yeniden yapılanmasında SPARK kullanılmasıdır (iFACTS – Interim Future Area Control Tools Support, bkz. http://www.nats.co.uk/article/90). SPARK Ada'nın alt kümesidir ve tasarımcıya programın önemli bileşenlerini kanıtlama özellikleriyle genişletilmiştir: sonlandırma, çalışma-anı istisnalarının varlığı, sonlu bellek kullanımı vb. [2]. Açıktır ki bu tür tasarım ve analiz yöntemi (İnşaanın doğruluğu) tasarımı SPARK ile başlanılmış olan sistemin güvenilirliğini oldukça arttıracak. Bununla birlikte, SPARK'ı geliştiren ve iFACTS'ı tasarlayan şirket PRAXIS, matematiksel yeterliliği olan çalışan istihdam etmekte zorluk çekmiştir (ve bu formal yöntemlerin daha çok öğretildiği İngiltere'de bile böyledir ).

CS (Computer Science – Bilgisayar Bilimi) öğrencilerinin açık olmaları gerektiği bir başka formal yaklaşım ise model kontrolü ve eşzamanlı (concurrent) sistemlerin tasarımı için doğrusal geçici mantıktır. Konunun, kritik-görev yazılımlarının merkezi olan, modern bir tartışması için bakınız [3].

Bilgisayar biliminin bir başka ihmal edilmiş alanı ise kayan-noktalı (floating-point) hesaplamadır. New York Üniversitesinde nümerik metodlar ve kayan-noktalı hesaplama dersi zorunlu olmalı, fakat bu zorunluluktan yıllar önce vazgeçildi ve şimdi çok az öğrenci bu dersi alıyor. Konu tüm bilimsel ve mühendislik yazılımları için hayati önemdedir ve çok hassastır. Bu, bilimsel programlamayla ilgili tüm derslerin gerekli bir parçası olarak düşünülebilir fakat böyle düşünüenler genellikle Matlab'ı evrensel programlama aracı olarak alırlar ve konuyu tamamiyle gözardı ederler.