Vlákno názorů k článku Porovnání systémů Linux a FreeBSD (2) od Clock - "Chyby v SMP zamykani vpodstate vubec debuggovat nejdou...

"Chyby v SMP zamykani vpodstate vubec debuggovat nejdou a nezbyva nez si cely kod precist a ujistovat se, ze je zamykani spravne."

Tento priklad demonstruje, ze v dnesni dobe bezne pouzivany vyvojovy cyklus "napis program - zkus jestli funguje - oprav nalezene chyby - zkus ho znovu - uvolni ho" je fundamentalne spatne. Zde se konecne ukazuje, ze psani BugFree(TM) kodu, neboli ze si po sobe kod peclive precteme a popremyslime, jestli je spravne (pripadne to nahradime nejaky strojovym popremyslenim), je jediny univerzalni nastroj, jak dosahnout semanticke spravnosti programu.

Ad "nahradime nejaky strojovym popremyslenim": No to je fajn. Jestli vymyslis algoritmus, ktery mi u jakehokoli programu dokaze alespon urcit, zda dobehne nebo ne, tak mi ho posli. Zverejnim ho a budu slavny ;-)))

Mel jsem na mysli formalni specifikace, verifikace a podobne veci co konceji na -ace.

A zkusil jsi to nekdy ? Teorie je to sice pekna, ale nezapomen ze program je nutne dokoncit v tomhle stoleti. Navic aby ti formalni verifikace fungovala, musis mit matematicky model pocitace a kernelu, coz nemas.