"Mi másra szeretnéd még? (Funkcionális nyelvekre még automatikus bizonyító rendszer is létezik, gondolom ezért írták haskellben.)"
Mondjuk objektum-orientáltra, de tényleg lényegtelen.
"A helyességbizonyítás nem mond semmit a teljesítményről, és a memóriafogyasztásról.
Attól függ, mi van a specifikációban. :) Egyébként valószínűleg ezt is szem előtt tartották."
Nyilván, csak az külön tudomány, nem része a helyességbizonyításnak.
"Szerintem arra nincs módszer hogy általános esetben egy többszálú alkalmazásról belássuk, hogy soha nem fog deadlock-ot, vagy egyéb párhuzamos szoftvernél előforduló betegséget kapni.
De van rá módszer. De csakúgy mint programozni, helyességet bizonyítani is hatványozottan nehezebb mint egyszálú programnál."
Tényleg nem kötözködni akarok, de áruld már el a módszer nevét, vagy adj egy linket ...