[nem-pl] Uwagi różne

["Paweł W. Olszta"]

Marcin 'Qrczak' Kowalczyk wrote:

>>No nie, to jest tak, że błąd w tym miejscu powienien wyskoczyć zawsze, 
>>jeśli kompilator nie potrafi sobie zinferować, że x jest różne od zera 
>>(np. bo zobaczy wcześniej odpowiedniego if'a albo assert (x != 0)).
> 
> Błąd kompilacji? Żaden język tego nie robi przy dzieleniu przez nieznaną
> liczbę! I słusznie: bo zwykle to, że wartość jest zawsze różna od zera,
> nie wynika z kodu w tak oczywisty sposób, żeby kompilator to zauważył
> (tym bardziej że reguły poprawności programu powinny być ścisłe, więc
> zauważenie musi być w jakiś ładnie specyfikowalny sposób, a nie "kiedy
> akurat kompilatorowi się uda").
> 
> Na przykład dana funkcja po prostu nigdy nie jest wołana z argumentami,
> z których wychodzi 0, tylko system typów nie jest w stanie tego opisać.

System typów nie, ale można sobie wyobrazić (na modłę Eiffel'a):

args_never_zero (x : int, y : int) : int {
   require { x != 0; y != 0 };
   ...
   def z = 1 / x + 1 / y;
   ...
   assert (x - y != 0);
   def ź = 1 / (x - y);
}

Ja rozumiem, że zasadniczo inferencja takich właściwości jest 
nierozstrzygalna, ale wyobrażam sobie rozstrzygalne i łatwo obliczalne 
ograniczenia problemu.

Tutaj nie chodzi o to, żeby kompilator wykrył, że programista zrobił 
błąd, tylko o to, żeby się upewnić, że programista przemyśłał to, co 
napisał.

Czyli coś w stylu komentarza rozumianego przez kompilator.

> A jeśli łatwo nie wynika, to jedyne, co programista może zrobić, to
> wstawić jawne sprawdzenie, które w przypadku zera rzuci wyjątkiem. Czyli
> zrobi dokładnie to samo, co dzielenie nie sygnalizujące błędu w czasie
> kompilacji. Więcej takich sytuacji i wkurzony programista po prostu
> zdefiniuje sobie funkcję, która robi
>    if (y == 0) throw DivideByZero
>    else x / y
> czyli nie zyskał nic, tylko stracił na czytelności.

Widzisz, w tym momencie peer reviewer zauważa, że wkurzony programista 
próbuje oszukać system i nie wydaje zgody na check-in. Poza tym, jak w 
przykładzie wyżej: zwykła asercja rozwiązuje problem.

> Dzielenie przez zero to tylko przykład.

Dokładnie. Jest tego dużo więcej. W ramach najprostszych przykładów mamy 
weryfikacja typów (w .NET na poziomie IL'a), nullness-checking, czy 
różne rodzanie abstrakcyjnych specyfikacji (poguglaj np. AsmL czy Fugue 
z Microsoft Research).

> Twoja filozofia jest sprzeczna z filozofią Erlanga

Pewnie tak ;]

> Bezpieczne to znaczy
> 1. procesor nie idzie w krzaki, błędy są zauważane przez rantajm
>    (antyprzykład: C i C++),
> 2. błędy wykonania są sygnalizowane, a nie maskowane (antyprzykład:
>    Perl).

Dla mnie bezpieczne, to znaczy korzystające ze zrozumiałych i jasnych 
reguł, które nie dopuszczają do sytuacji nie będących jasno zapisanymi w 
kodzie źródłowym. Antyprzykład: buffer overflows w C.

-- 
If you're not confused, you're misinformed.