Post by J. J. LodderPrecies, je schrijft wiskundig gezien triviale programmas,
waarvan je in een eindig aantal stappen kan verifieren
dat ze zullen stoppen of in een loop zullen raken.
Niet verifiëren, niet zeker weten, maar wel ordelijk werken zodat ze
kans groot is dat het goed gaat. En in kleine stapjes steeds dingen
toevoegen en tussendoor weer testen, zodat ALS er iets in de soep
loopt je vrijwel precies weet waar je de fout moet zoeken.
Post by J. J. LodderJe zou dat desgewenst zelfs machinaal kunnen verifieren.
Sommige van dat soort programmas komen zelfs met een correctheidsbewijs.
[come with; brrr, anglicisme. Zijn voorzien van, gaan vergezeld door]
In al die jaren dat ik (een deel van m'n tijd, soms fulltime) heb
geprogrammeerd heb ik diverse keren geknokt tegen hardnekkige bug, van
die leuke die precies op het punt waar het fout ook je hele debugger
aan gort gooit, zodat je keer op nog steeds niks weet over de
oorzaak), en al die tijd wist ik van die verhalen over die
correctheidsbewijzen, maar in de praktijk heb je daar HELEMAAL NIETS
aan, ze geven geen ondersteuning bij de noeste arbeid, anderhalve je
de tiefus zoeken met een deadline op je nek zonder ook maar IETS
zinnigs te kunnen zeggen over hoe lang het nog duurt, dat is niet fijn
werken. Maar ik heb het uiteindelijk altijd gewonnen, dat wel. Met
tools en logisch nadenken en ordelijk werken, maar NIET met wiskunde
of informatica. Dat is theoretisch geneuzel waar niemand mee geholpen
is.
Idem met die wiskundige theorieën over databates. Allemaal gelul. En
objectgericht programmeren is grotendeels ook alleen maar onhandig en
niet verhelderend of kwaliteitsverhogend.
Post by J. J. LodderTegenwooordig, sinds Goedel, zijn we gewend
aan dit soort limitatieve resultaten,
maar toen dit soort dingen voor het eerst ontdekt werd
kwam dat als een grote verrassing,
en (voor sommigen) ook als een grote schok,
Geen idee wie Goedel is (geeft ze seksuele voorlichting? :) ), maar
die zoek ik op:
https://nl.wikipedia.org/wiki/Kurt_G%C3%B6del
==
In 1931 bewees Gödel namelijk dat binnen elk zelfconsistent recursief
axiomatisch systeem, dat krachtig genoeg is om de rekenkunde van de
natuurlijke getallen te beschrijven (Peano-rekenkunde), er tenminste
een ware stelling over de natuurlijke getallen bestaat, die niet
bewezen kan worden op basis van de axioma's van dit systeem.
==
Geweldig! Dat zal ze leren.