Użytkownik "M.M." napisał w wiadomości grup
dyskusyjnych:c8c46028-ecf9-454b-bb5d-75458b6ea66f@go
oglegroups.com...

>Inny przykład, program do translacji języków naturalnych. Dlaczego
>chciałbyś używać gorszy program niż lepszy?

Dlaczego uważasz, że dla w/w programów da się ustalić relację liniowego
(pół)porządku?

A praktycznie: program X zwykle daje ładniejszy tekst, ale za to przetwarza
dane w chmurze, wysyłając je na serwer nie-wiadomo-gdzie. Program Y daje
przyzwoitą jakość i przetwarza lokalnie. Który wybierzesz do przetłumaczenia
tekstu przetargu? A który do przetłumaczenia tekstu na publicznie dostępną
stronę WWW?

>Następny problem: gra w szachy. Dlaczego używać słabszego programu niż
>silniejszego? Można mnożyć...

Bo np. silniejszy program zawsze wygrywa, więc nie ma fun-u?
Można dzielić...

>się konkretyzuje. Bez względu na to jak się skonkretyzuje, to ciężko
>dokonać takiego dowodu formalnego.

Problem, IMO, leży w czym innym: dowody formalne zapobiegają tylko niektórym
błędom. A same z siebie mogą być błędne. Więc stwarzają złudną iluzję
bezpieczeństwa.

Ok. Zastąpmy "dowodzenie formalne" przez "pasy bezpieczeństwa". Oczywiście,
pasy ratują życie itd. Ale /pomimo/ pasów zdarzają się śmiertelne wypadki.
Więc np. jazda na podwójnym gazie, 200 km/h w terenie zabudowanym, w gęstej
mgle i pod prąd nie jest bezpieczna nawet jeżeli PASY SĄ ZAPIĘTE. Podobnie
pisanie super-odpowiedzialnych programów przez tylko jednego programistę,
bez testów - NAWET Z UŻYCIEM FORMALNYCH DOWODÓW POPRAWNOŚCI - nie jest moim
zdaniem dobrym pomysłem. I niekoniecznie dlatego że będą błędy.