Kod gwarantowany

Ariel Davis

Adam Chlipala, docent informatyki na MIT, uważa, że ​​istnieje lepszy sposób na pisanie programów komputerowych.

Większość programów wyświetla tylko listę operacji, które komputer powinien wykonać, gdy otrzyma określone typy danych. Programista musi pisać testy, aby określić, czy program robi to, co powinien, a ponieważ praktycznie niemożliwe jest przewidzenie wszystkich sposobów użycia programu, większość programów ma błędy.

Chlipala preferuje tzw. programowanie funkcjonalne. Zamiast łączyć ze sobą imperatywne polecenia, programista funkcyjny definiuje zestaw funkcji lub matematycznych relacji między wejściami i wyjściami. Zasadniczo programowanie funkcjonalne wyraża to, co robi program, jako zestaw równań.

Myślenie o programach jako o kombinacjach funkcji może być nieintuicyjne, ale dla ludzi, dla których pracuje, jest to naprawdę niesamowity sposób na zwiększenie produktywności, mówi Chlipala. Po pierwsze, może wyeliminować testowanie. Programy funkcjonalne są tak matematycznie precyzyjne, że stosunkowo łatwo jest je zweryfikować lub automatycznie udowodnić, że robią to, co powinny.

Jeden z Chlipali główne zainteresowania naukowe poszerza zakres automatycznej weryfikacji. Na przykład, opracowane przez niego i współpracowników narzędzia weryfikacyjne umożliwiły stworzenie pierwszego systemu plików — części systemu operacyjnego, która zarządza przechowywaniem danych — gwarantującego, że dane programu nie zostaną utracone podczas awarii systemu.

Kolejną zaletą języków funkcjonalnych jest to, że eliminują one wiele pracochłonnych prac programistycznych. Znowu, ponieważ programy funkcjonalne są tak precyzyjne, kompilatorom — programom, które zamieniają kod w pliki wykonywalne — łatwo jest dowiedzieć się, jak sprawić, by działały jak najefektywniej.

Jednym z najpopularniejszych narzędzi Chlipali jest język funkcjonalny o nazwie Ur/Web — jedyny język programowania, który pozwala programistom określić wszystkie funkcje aplikacji internetowej w jednym programie. Kompilator Ur/Web następnie automatycznie generuje kod XML, kod JavaScript i zapytania do bazy danych niezbędne do wdrożenia aplikacji. Zapewnia również prawidłowe współdziałanie tych różnych komponentów.

Ur/Web jest podobny do innych języków funkcjonalnych, ale dodaje funkcje bezpieczeństwa, które umożliwiają automatyczne zatykanie luk powszechnie występujących w aplikacjach internetowych. Na przykład może zagwarantować, że część kodu zaimportowana do jednej sekcji strony (takiej jak reklama) nie będzie mogła szpiegować innej (takiej jak narzędzie kalendarza).

Jak wielu informatyków po trzydziestce, Chlipala próbował swoich sił w pisaniu gier wideo w szkole średniej. Ale to przedsięwzięcie szybko poprowadziło go w innym kierunku. Kiedy był na pierwszym roku, jego próby pisania gier dla kalkulatora graficznego Texas Instruments doprowadziły go do opracowania kompilatora dla tego urządzenia.

W dalszym ciągu koncentrował się na kompilatorach na Uniwersytecie Carnegie Mellon, a podczas pierwszego semestru studiów magisterskich na Uniwersytecie Kalifornijskim w Berkeley jego przyszły promotor zapytał go, czy chciałby przyczynić się do projektu komputerowego. wspomagana weryfikacja. Chlipala natychmiast się uzależnił.

Istnieje pewien rodzaj paranoidalnej osobowości, która uzależnia się od tego rodzaju pracy, a to zdecydowanie ja, mówi. Nie ma wielu rzeczy, które są absolutnie pewne na tym świecie, ale kiedy robisz sprawdzone maszynowo dowody dotyczące programów, jesteś całkiem blisko.

ukryć