On Tuesday, March 31, 2015 at 7:08:24 PM UTC+2, slawek wrote:
> Użytkownik "M.M." napisał w wiadomości grup
> dyskusyjnych:
>
> >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?
Da się. Bierzemy N programów, M tekstów, K ludzi. Każda osoba czyta
przetłumaczony tekst i wystawia ocenę od zera do np 10. Sumujemy
punkty. Więc w ogóle można porównywać program do tłumaczenia, a na
podstawie kodu nie można.


> 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ć...
Jak już odbiegamy, to też nie zawsze. Weźmiemy np. 20 programów i
zrobimy turniej każdy z każdym. Może się okazać, że zwycięzca
turnieju przegrywa z przegranym - ale to tylko na marginesie.

>
> >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.
Soft do sterowania rakietami podobno
pisało osiem niezależnych zespołów. Wszystkie osiem wersji softu
działało równolegle. Wyjście tych wszystkich wersji trafiało do systemu
głosowania. Nawet jeśli tylko 2 wersje dały dobrą odpowiedź, a
pozostały złą ale różną od siebie, to system jako całość działał.


Pozdrawiam