211service.com
Garantuotas kodas
Arielis Davisas
Adamas Chlipala, MIT kompiuterių mokslo docentas, mano, kad yra geresnis būdas rašyti kompiuterines programas.
Daugumoje programų tiesiog pateikiamos operacijos, kurias kompiuteris turi atlikti, kai gauna tam tikro tipo duomenis. Programuotojas turi parašyti testus, kad nustatytų, ar programa atlieka tai, ką turėtų, ir kadangi beveik neįmanoma numatyti visų būdų, kaip programa gali būti naudojama, daugumoje programinės įrangos yra klaidų.
Chlipala pirmenybę teikia vadinamajam funkciniam programavimui. Užuot sujungęs būtinas komandas, funkcinis programuotojas apibrėžia funkcijų rinkinį arba matematinius ryšius tarp įvesties ir išvesties. Iš esmės funkcinis programavimas išreiškia tai, ką programa daro kaip lygčių rinkinį.
Mąstymas apie programas kaip funkcijų derinys gali būti neintuityvus, tačiau žmonėms, kuriems jos veikia, tai tikrai nuostabus produktyvumo didiklis, sako Chlipala. Viena vertus, tai gali panaikinti bandymus. Funkcinės programos yra tokios matematiškai tikslios, kad palyginti paprasta jas patikrinti arba įrodyti, kad jos daro tai, ką turėtų, automatiškai.
Vienas iš Chlipalų pagrindiniai moksliniai interesai plečia automatinio tikrinimo sritį. Pavyzdžiui, jo ir kolegų sukurti tikrinimo įrankiai leido sukurti pirmąją failų sistemą – operacinės sistemos dalį, kuri valdo duomenų saugojimą – užtikrino, kad sistemos gedimo metu nebus prarasti programos duomenys.
Kitas funkcinių kalbų pranašumas yra tai, kad jos pašalina daug programavimo rūpesčių. Vėlgi, kadangi funkcinės programos yra tokios tikslios, kompiliatoriams – programoms, kurios paverčia kodą vykdomaisiais failais – lengva išsiaiškinti, kaip užtikrinti, kad jos veiktų efektyviausiai.
Vienas iš populiariausių Chlipala įrankių yra funkcinė kalba, vadinama Ur/Web – vienintelė programavimo kalba, leidžianti programuotojams nurodyti visas žiniatinklio programos funkcijas vienoje programoje. Tada Ur/Web kompiliatorius automatiškai generuoja XML kodą, JavaScript kodą ir duomenų bazės užklausas, reikalingas programai įgyvendinti. Tai taip pat užtikrina, kad šie skirtingi komponentai tinkamai sąveikauja.
„Ur/Web“ yra panašus į kitas funkcines kalbas, tačiau prideda saugos funkcijų, leidžiančių automatiškai užkimšti žiniatinklio programose įprastas skyles. Pavyzdžiui, ji gali garantuoti, kad dalis jo kodo, importuoto į vieną puslapio skiltį (pvz., reklamą), negalės šnipinėti kitos (pvz., kalendoriaus įrankio).
Kaip ir daugelis 30 metų sulaukusių kompiuterių mokslininkų, Chlipala vidurinėje mokykloje išbandė savo jėgas rašydamas vaizdo žaidimus. Tačiau ši įmonė greitai nuvedė jį kita linkme. Kai jis buvo pirmakursis, jo bandymai rašyti žaidimus „Texas Instruments“ grafiniam skaičiuotuvui paskatino jį sukurti įrenginio kompiliatorių.
Būdamas Carnegie Mellon universiteto bakalauras ir toliau daugiausia dėmesio skyrė kompiliatoriams, o būdamas Kalifornijos universiteto Berklio universitete magistrantūros studentas, būsimas baigiamojo darbo patarėjas jo pirmąjį semestrą paklausė, ar jis nenorėtų prisidėti prie projekto, susijusio su kompiuteriais. padedamas patikrinimas. Chlipala iškart užsikabino.
Yra tam tikra paranojiška asmenybė, kuri tampa priklausoma nuo tokio darbo, ir tai tikrai esu aš, sako jis. Šiame pasaulyje nėra daug dalykų, kurie būtų visiškai tikri, bet kai atliekate mašininiu būdu patikrintus programų įrodymus, gana arti.