Onko olemassa 2021 täysin robustia tietokone-ohjelmaa?

[Jere Sumell]

Keskustelin taannoin jokin kuukausi takaperin shakkitietokoneen ohjelmoinnista Ohjelmointiputkassa avaten siitä oman säikeensä siellä, niin tuli tuollainen kysymys mieleeni, että voiko tietokone-ohjelma tai algoritmi olla käytännössä koskaan 100% robusti?

Kun tuli juttua ohjelmoinnin teoriassa koodin vaativusmääritelmistä, eli lähinnä että ohjelmakoodi on

a.) mahdollisimman uudelleenkäytettävää (re-usability), mikä yleensä saavutetaan modulaarisoimalla top-down -menetelmällä pilkommalla suuremmat ongelmat yhä pienempiin osa-ongelmiin, kunnes jäljellä on enää niin yksinkertainen metodi, joka todella on moneen tilanteeseen sopiva.
b.) Mahdollisimman vähän koodin toistoa sisältävää (code redudancy), lähinnä turhien toistojen ja ehtolauseiden minimointia, mutta proseduraalisissa ohjelmoinnissa ja rakenteisessa ohjelmoinnissa esiintyy uudelleen toistoa paljonkin, ja mitä mennään ohjelmoinnin historiaan, niin 1950/1960 -luvulla tämä ei ollut mitenkään voinut olla vaatimuksena.

Päädyin miettimään tuollaista, että voiko ylipäätään, jos ongelma on algoritmisesti ratkeava suotuisassa ajassa, kuinka todellista reaalimaailman sovelluksissa ohjelmiston robustisuus käytännössä toteutuneena on?

Päädyin pohdinnassa siihen, että jos ottaa kaikkien ohjelmien emo/isä-ohjelman tarkasteluun, jollaisena käyttöjärjestelmää voidaan ainakin jossain määrin pitää, kun tietokoneella oikein voi tehdä mitään järkevää ilman, että siinä olisi asennettuna jokin kyseisessä sähkölaitteessa toimiva käyttöjärjestelmä, niin Windows nyt ei ainakaan ole lähelläkään robustia, mutta pohtisin, että mahtoiko 1990 vuonna ensimmäinen Linux-versio olla melko lähellä sitä?

Linuxin kehittäjäyhteisö on paisunut ja kehitystyö niin laajaksi, että Linux:kaan, jota voi pitää hyvänä käyttöjärjestelmänä tekniikkansa osalta, niin ei tämäkään mikään täysin robusti käyttöjärjestelmä-ohjelmisto ole käsittääkseni?

Tästä nousee siis kysymys, onko mahdollista ohjelmoida käyttöjärjestelmää jollekin sähkölaitteelle, joka olisi täysin robusti?

Varmaan mikro-ohjelmointitasolla mitä joskus joku täälläkin palstalla totesi, että varmaan prosessoritehtaalla mikro-ohjelmoitu C-kääntäjä Intelin tehtailla poltetaan piirilevyyn kiinni, niin ne varmaan aika tavalla järkeviä analyyseja virhesyötteistä antaa, mutta korkeamman tason vähän kompleksiemmista ohjelmista, en ole nähnyt missään alan kirjallisuudessa ohjelmointiteoriasta puhuttaessa, että koodin pitäisi olla parhaimmillaan myös täysin robusti ratkaisu.

Näin ei varmaan käytännössäkkään ole? Onko muilla palstalaisilla tähän jotain ajatusta heittää?

[JaniAlander]

Hmm vierastan vähän tuota robust sanaa, mikähän olisi hyvä suomenkielinen ilmaisu tässä yhteydessä. Ensimmäiset mieleen tulevat olisi sorttia "jämäkkä", "kestävä", "vikasietoinen"....

[epiphone]

https://www.sanakirja.org/search.php?id=68316&l2=17

Tuollainen tuli googlella vastaan...

[JaniAlander]

Vankka olisi tässä yhteydessä ehkä paras...

[_Pete_]

On:

speksi: tulosta loputtomasti "Moi" kunnes ohjelma keskeytetään

Koodia: [Valitse]

10 print "Moi"
20 goto 10

Toimii täysin robustisti speksien mukaan

[AimoE]

Näin kerran manuaalin jostain 50-60-luvulta. Siinä esiteltiin ohjelmointikieli tms. nimeltään "Auto Code II" tietokoneeseen, joka on ollut jos ei aivan ensimmäinen Suomessa, niin ihan ensimmäisiä. TKK:n käytössä se taisi olla eka. Kieli oli jotain konekielen ja assemblerin väliltä; silloin ei vielä ollut assemblereita. Esittelytekstissä kehuttiin että tämän uuden järjestelmän avulla verraton kokematonkin ohjelmoija voi nopeasti oppia kirjoitamaan virheettömiä ohjelmia (ihan tarkkaa sanamuotoa en pääse enää tarkistamaan, mutta aikalaillanoinse oli). Siitä on riittänyt naurun aiheeksi ja riittää vieläkin.

[Jere Sumell]

On:

speksi: tulosta loputtomasti "Moi" kunnes ohjelma keskeytetään

Koodia: [Valitse]

10 print "Moi"
20 goto 10

Toimii täysin robustisti speksien mukaan

No tuo nyt on, mutta sitten herää kysymys, kuinka järkevä tai hyodyllinen ohjelmaa suorittaessa tuo on. Eihän pelkän tervehdystekstin tulostaminen loputtomiin kovinkaan mielekkäältä ohjelmalta vaikuta.

[Jere Sumell]

Hmm vierastan vähän tuota robust sanaa, mikähän olisi hyvä suomenkielinen ilmaisu tässä yhteydessä. Ensimmäiset mieleen tulevat olisi sorttia "jämäkkä", "kestävä", "vikasietoinen"....

Kyllä tuo vakaa, vankka aika lähellä on jos ei tykkää robusti-sanaa itseään käyttää.

Yleensä akateemisissa teksteissä on tuo robusti, mutta kyllähän se vankka, kestävä, kun viittaan esimerkiksi Tieteen Termipankin Wiki-lähteeseen, jossa on myos tuo virhesyotteiden mielekkäät analyysit.

https://tieteentermipankki.fi/wiki/Nimitys:robusti

[_Pete_]

On:

speksi: tulosta loputtomasti "Moi" kunnes ohjelma keskeytetään

Koodia: [Valitse]

10 print "Moi"
20 goto 10

Toimii täysin robustisti speksien mukaan

No tuo nyt on, mutta sitten herää kysymys, kuinka järkevä tai hyodyllinen ohjelmaa suorittaessa tuo on. Eihän pelkän tervehdystekstin tulostaminen loputtomiin kovinkaan mielekkäältä ohjelmalta vaikuta.

Niin kuten tämän tapauksen määrittelystä näkee niin se juuri niin järkevä ja hyödyllinen kuin pitääkin.

[kamara]

Kyllähän monimutkaisiakin ohjelmia voi todistaa oikein toimivaksi, mutta silloin todistuksenkin pitää olla virheetön. Eli sekin olisi parempi tehdä koneellisesti – ainakin osittain.

[AimoE]

Kyllähän monimutkaisiakin ohjelmia voi todistaa oikein toimivaksi, mutta silloin todistuksenkin pitää olla virheetön. Eli sekin olisi parempi tehdä koneellisesti – ainakin osittain.

Ainakin osittain, joopa joo. Sanotaan että Gödel tuli hulluksi todistettuaan että kaikkia matemaattisia totuuksia ei voi todistaa (tulos tunnetaan nimellä Gödelin epätäydellisyyslause). Vain hitunen kaikista matemaattisen logiikan totuuksista voidaan matemaattisen logiikan säännöillä todistaa, ja ohjelman oikein toimivaksi todistaminen kuuluu juuri tähän todistusten luokkaan.

Gödelin täydellisyyslause kuului ainakin minun aikanani lukion oppimäärään, mutta Gödelin epätäydellisyyslause todistuksineen käydään edelleenkin läpi vasta yliopistolla, matemaattisen logiikan kurssilla.

[AimoE]

Tuli mieleen että "hitunen" on aika hämäävä sanonta, joten tarkennan sitä hitusen.

Todistettavien tosien väitteiden ja kaikkien tosien väitteiden keskinäistä suhdetta voi jossain määrin verrata rationaalilukujen ja reaalilukujen suhteeseen. Irrationaalilukuja on vaikea käsitellä täsmällisesti, joten kutakuinkin kaikki laskenta tehdään rationaaliluvuilla, joiden arvo on mahdollisimman lähellä tarkoitettua reaalilukua. Kuitenkin jos heitetään tikkaa lukuakselille, niin todennäköisyys osua johonkin rationaalilukuun on niin infinitesimaalinen, ettei sitä voi mitata, joten todennäköisyys on käytännössä nolla. Ihan tasan nolla se ei kuitenkaan ole, vaan eroaa nollasta hitusen. Silti, vaikka rationaalilukuun osuminen on näin epätodennäköistä, rationaaliluvut ovat olemassa ja niiden käyttö on mielekästä.

Todistettavien totuuksien todistaminen on myöskin mielekästä, vaikka niitä onkin vain hitunen verrattuna niihin joita ei voi todistaa.

Ohjelmien oikeaksi todistamisessa oleellisinta on kuitenkin se, mistä Pete huomautti. Silloinkin kun voidaan todistaa, että ohjelma toimii täsmälleen speksin mukaan, niin käyttäjän kannalta ohjelma saattaa silti toimia väärin.

[kamara]

Kiitos AimoE tästä piristävästä informaatiosta. 

[jekku]

Ja kuten vanhat miehet sanovat: "joka pävä jotain", minulle robusti on aina tarkoittanut jotain "kirveellä veisteltyä" - en koskaan ollut vaivautunut tarkistamaan

[Jere Sumell]

Ohjelmien oikeaksi todistamisessa oleellisinta on kuitenkin se, mistä Pete huomautti. Silloinkin kun voidaan todistaa, että ohjelma toimii täsmälleen speksin mukaan, niin käyttäjän kannalta ohjelma saattaa silti toimia väärin.

Tuo on hyvä huomio! Tuossa kohtaa, kun ohjelma toimii käyttäjän kannalta eri tavalla, mitä pitäisi, yleensä ohjelmistokuvauksen määrittelyssä suunnitteluvaiheessa jotain vikaa, tai sitten ohjelmoija ei ole ymmärtänyt oikein jotain asiaa.

Ja sitten taas jos mennään lähemmäs rautatasoa, niin onhan ohjelmia, jotka ovat virheellisiä, mutta saattavat mennä ongelmitta kääntäjän tai tulkin läpi, ja sitten ohjelmakoodikin voi olla syntaktisesti, eli kieliopillisesti kaikkien sääntöjen mukaan virheettömästi laadittu, kirjoitettu, mutta sitten kun kääntäjä myös tarkistaa semantiikkaankin liittyviä asioita, niin yleensä ne ei mene kääntäjästä tai tulkista läpi, jos se kääntäjä tai tulkki on oikein ohjelmoitu ymmärtämään niitä korkean kielen niistä puhutaan produktioista, kun siinä leksikaalisessa analyysissa sitä produktioista jäsennetään se kielioppi-sääntöpuu, kun kääntäjää ohjelmoidaan.

Tässäkin ketjussa nyt tullut oikein mitään kovinkaan myötäpuhuvia argumentteja, että kovinkaan kompleksisia ohjelmistokokonaisuuksia ei voi täysin vakaina, tai itse tykkään tuosta robusti sanasta, niin robusteina pitää, ja kuten tuossa aiemmin todettiin, niin teustauskin pitäisi tehdä virheettömästi, ja kun ajatellaan, että ohjelmointi on aina käsityötä, ihmisen älyllisen ponnistelun tulos, ohjelmointia ei voi yleisesti ottaen automatisoida, että sähkölaite tai jos nyt tarkennetaan tietokone alagenrenä noista sähkölaitteista, niin taitaa olla ihmisen elinkaaren loppuun saakka tämä kysymys robustista tietokoneohjelmasta auki jäävä loppuun saakka.

Ei ole tiettävästi olemassa ihmisen historian huomioon ottaen vielä elossa ollutta ihmistä, jonka ajattelu ja päättely ja toiminta toimisi täysin virheettömästi, ja se on inhmillinen piirre. Onko niin, että kun ohjelmointi on ihmisen älyllisen aivotyöskentelyn käsityönä tapahtuvan toiminnan tulos, ja ihmiselle on luontaista tehdä virheitä, niin johtopäätöksenä että tietokoneohjelmoinnissa siis on ripaus inhimillisä piirteitä olemassa enemmän, mitä nyt äkkiseltään voisi kuvitella?

[AimoE]

Jaa, minä ajattelin että robusti ja oikein toimiminen ovat kaksi eri asiaa. Vastasin kamaralle, kun aloitin sen haaran. Robusti ei minulle tarkoita täysin virheetöntä. Vankka on ihan hyvä käännös.

[Jere Sumell]

Jaa, minä ajattelin että robusti ja oikein toimiminen ovat kaksi eri asiaa. Vastasin kamaralle, kun aloitin sen haaran. Robusti ei minulle tarkoita täysin virheetöntä. Vankka on ihan hyvä käännös.

Ymmärsin kyllä hyvin sinun lähestymistapasi, eli ihminen tai toinen tietokone, joka käyttää ohjelmaa, että eri asia on, toimiiko ohjelma käyttäjän kannalta on se sitten ihminen tai toinen tietokone, oikein.

Tämäkin Peten esittämä moikkailu loputtomiin tietokoneenruudulla ei oikein tosiaan kuten totesin, vaikuta mielekkäältä tietokoneohjelmalta ja jo alkuperäisessä viestissäni taisin mainita "vähän komplesisemman" -tietokoneohjelman ehkä vähän tarkoittaen myös sitä, että sillä olisi jotain reaalimaailman käyttöä.

Onhan tuo Peten ohjelma robusti, en sitä kiistä, mutta onko tuttailulla tietokoneen käyttäjää ohjelmoituna tietokoneen sen tekemänä mitään kovinkaan hyödyllistä tarkoistusta?

Maailma on täysi ohjelmia, ja paljoon jo löytyy reaalimaailmassa tietokoneen kykeneviä peruskäyttäjän näkkulmasta ohjelmia, jotka pystyvät tekemään kaikenlaista, joten sellaista lienee enää turhaa lähteä ohjelmoimaan ainakaan nollasa. Lopulta meidän ihmisten elämässä ei kysymys kuulukaan "Onko ohjelma täydellinen ja vakaa toimiessaan", mitä tämä järjestelmä on lähtenyt muovautumaan jo todella kauan sitten vapaan markkinatalousjärjestelmän suuntaan, mitä siihen vapaan markkinatalousjärjestelmän ehkä jotkut siihen oppineet puhuvat ihmisen luontaisesta ahneudesta, ja vaikka kuinka Marxin tekstit olisi tuttuja, niin  ihminen ei koskaan saavuta minkään teorian tai käytännönkään maksimi-ideaalista optimitilannetta. Ihminen on vajaa luomus. (vrt. Bill Gates, Microsoftin perustaja, pitkään maailmassa ihmisen sen hetkisen suurimman omaisuuden luonut juristi-opinnot Haravardissa keskeyttänyt tietokone-ohjelmoija-harrastaja, joka loi tietokone-ohjelmoillaan ihmisen historian merkittävimmän omaisuuden.)

Yritetään tässä silti navigoida tämä elämä toivottavasti humaaniin loppuun vanhuudessa, on täällä paljon hienoakin. Tietotekniikka ja nopeat nettiyhyteydet, mitä ihminen on kehittänyt, on tuonut mukanaan paljon hyvääkin, mutta ennen tosiaan jotkin asiat olivat paremmin: Ennen sentään piti ostaa fyysinen mediatuote, jos halusi kuunella jotain artistia tai musiikkiakin enemmän, ja edes 2000-luvun millenumtaitteen ohessa kotimaiset miesten lehtien julkaisukin lakkautettiin kustannustehokkaista syistä. Nykynuoriso ei edes tiedä, mikä on "äänilevy", tai "kotimainen pornolehti". Nämä asiat oli siihen maailmaan aikaan paremmin, kun ihmisllä oli mediat mitä me seurasimme, niin televisio, radio, printti-sanomalehdet, ja printti-aikakauslehdet.

[ilkant]

Kyllähän monimutkaisiakin ohjelmia voi todistaa oikein toimivaksi, mutta silloin todistuksenkin pitää olla virheetön. Eli sekin olisi parempi tehdä koneellisesti – ainakin osittain.

Kauan sitten perehdyin jonkin verran ohjelmien oikeaksi todistamiseen tieteellisesti. Oli aika mutkikasta silloin. Monisteet ovat jo kadonneet. Netissä on varmaan tietoa noista menetelmistä. Silloin tuli myös mieleen, että tuollainen laaja analyysi kannattaisi tehdä koneella. Millaisia ohjelmia on tarjolla?