On 28/03/2015 10:10, Maciej Sobczak wrote:
> W dniu piątek, 27 marca 2015 21:25:34 UTC+1 użytkownik Andrzej
> Jarzabek napisał:
>
>> Ale może właśnie potrafią wyspecyfikować, ale niekoniecznie w
>> języku formalnym.
>
> To skąd wiedzą, że dobrze wyspecyfikowały? Mają przeczucie?

Stąd, że się na tym znają.

>> Albo nawet, co jest też częste, nie potrafią co prawda
>> wystarczająco precyzyjnie wyspecyfikować, ale programista potrafi
>> dojść do tego poprzez zadawanie pytań, zrozumienie celu jaki ma
>> realizować program i posługiwanie się przykładami.
>
> I napisać funkcję sort?

W praktyce funkcję sort pisze się bardzo rzadko.

>> No więc właśnie algorytm sortowania to taki wdzięczny temat dla
>> metdo formalnych
>
> Tak. Metody formalne rozwija się po to, żeby wdzięcznych tematów było
> coraz więcej.

Być może, nie znaczy to jednak, że na obecnym etapie rozwoju jest sens
się nad tym zastanawiać w ogólnym przypadku.

>> Niestety w praktyce zwykle miewa się do czynienia z bardziej
>> skomplikowanymi przypadkami.
>
> Zgadza się. I co, wtedy się łatwo testuje?

Wtedy da się w praktyce testować - przez co rozumiem osiągnięcie
akceptowalnej niezawodności przy akceptowalnych kosztach.

>>> Zgadzam się, że to jest problem. Metody formalne są ciałem obcym
>>> w branży, bo nie pasują do dotychczas przyjętych wzorów pracy.
>>
>> Bo się nie nadają do realizacji tych zaań, które zazwyczaj się
>> realizuje.
>
> Ale testy też się nie nadają, tylko łatwiej to ukryć pod pozorem, że
> się je robi.

Ale jak najbardziej się nadają, bo testowane programy działają
wystarczająco często i per saldo zarabiają.

>> Konsensus jest taki, że metody formalne albo w ogóle nie nadają się
>> do zastosowania większości problemów, albo są nieopłacalne.
>
> Czyj konsensus? Bo na razie ustaliliśmy, że punkty widzenia są
> różne.

Konsensus, który obserwuję jako osoba pracująca od iluś tam lat przy
tworzeniu komercyjnego oprogramowania.

>> Jeśli konsensus się myli, to byłoby bardzo duże zainteresowanie
>> tym, jak by to zrobić w praktyce tak, żeby się opłacało.
>
> No więc ja rozumiem, że zainteresowanie jest.

Ja rozumiem, że jest głównie w tych nielicznych niszach, gdzie istnieje
uzasadnione podejrzenie, że się da.

>> Tyle że na razie udaje się to jedynie w specyficznych niszach.
>
> Bo tylko w specyficznych niszach się próbuje to robić. W pozostałych
> niszach może nawet nie być wystarczającej świadomości, że jest to
> możliwe.

Świadomość istnienia czegoś takiego jak metody formalne raczej jest, to,
czy jest dodatkowo opłacalne to raczej bym powiedział, że problem leży w
braku wiedzy czy rzeczywiście jest, a nie w tym, że jest, ale ludzie z
branży o tym nie wiedzą.

Noo chyba że masz matematyczny dowód na to, że metody formalne są opłacalne?

>> Jeśli uważasz, że dałoby się stosować te metody w ogólnym
>> przypadku, to np. ja byłbym bardzo zainteresowany - jak?
>
> Nie wiem. Nie wiem nawet, czy to jest dobre pytanie. Bo zamiast
> szukać jednej metody do zastosowania w ogólnym przypadku, może trzeba
> szukać szczególnej metody do każdego przypadku osobno. Ja wiem, że
> korporacje tego nie lubią, bo im to utrudnia zarządzanie zasobami
> metodą "zatrudnijmy 20% programistów więcej".

Może nie lubią dlatego, że przypadków jest dużo i wymyślanie nowej
metody byłoby zarówno bardzo kosztowne jak i bardzo ryzykowne - bo
problem trzeba rozwiązać, a nową metodę po pierwsze nie wiadomo, czy się
w ogóle uda znaleźć, a po drugie nie wiadomo ile to zajmie.

>> Ale właściwie co to ma do rzeczy? Firma nie ponosi straty jeśli
>> pracownik nie idzie do pierdla? Jak ktoś dostaje albo nie dostaje
>> premii to znaczy że są albo nie ma testów?
>
> Sam napisałeś, że to wszystko wynika z zarządzania ryzykiem. Powyżej
> masz input do tego zarządzania. Outputem jest wybór metod pracy.

Kompletnie nie widzę jak się to ma do tego, co pisałeś wcześniej.
Instytucje finansowe zajmują się zarabianiem pieniędzy, i generalnie
wszystkim od programisty aplikacji do prezesa raczej zależy, żeby
aplikacje zarabiały pieniądze, a nie je traciły. A straty z błędów są
jak najbardziej realne, w zależności od ontologicznego podejścia do
pieniędzy.

>> Da się, bo sukces testowania to nie jest 100% wyeliminowanie
>> szansy błędu, tylko redukcja ryzyka strat w takim stopniu, żeby
>> opłacało się to firmie.
>
> Zgadza się. Coś jak z pytaniem czy dziecko nauczyło się tabliczki
> mnożenia a ono odpowiada, że nauczyło się tyle, żeby w opłacalnym
> stopniu zredukować ryzyko wpadki. No to nauczyło się czy się nie
> nauczyło?

Praktycznie nauczyło się w wystarczającym stopniu. A historii Powstania
Styczniowiego dziecko nauczyło się wtedy, kiedy potrafi odpowiedzieć na
dowolne pytanie dotyczące jakiegokolwiek znanego światowi naukowemu
historycznego żródła mówiącego cokolwiek o Powstaniu Styczniowym, czy
jeśli ma odpowiednio dużą szansę, że odpowie na pytanie na pytanie z
tematu zadane przez nauczyciela?

>> Jak konkretnie by to wyglądało w przypadku takiego programu, jaki
>> opisałem?
>
> Złe pytanie. Tego programu jeszcze nie ma, więc nie ma takiego
> przypadku. :-) Przypadkiem może być problem do rozwiązania, np.
> "system tradingowy". Mam opisać jak się to robi od początku? No więc
> bierze się białą tablicę i pisak, a potem... ;-)

Program jest, coś robi, został napisany w warunkach jakiejś potrzeby i
był modyfikowane w warunkach zmieniających się potrzeb. Moje pytanie
jaką byś zaproponował metodę działania zamiast tej, która faktycznie
została zastosowana i doprowacziła do powstania programu takiego, jaki jest.

> Ja wiem, że to jest niemodne podejście. Teraz się od razu nap...la
> kod, zanim jeszcze będzie wiadomo, co program ma robić.

Widziałem wiele sytuacji, gdzie zaczęto od wzięcia białej tablicy i
pisaka, ale nigdy nie skończyło się to stworzeniem programu z dowodem
formalnym.

>> Ale niekompletne testy są też użyteczne, w sensie takim, że
>> realnie redukują ryzyko
>
> Jak realnie? Możesz to wyrazić w liczbach? Jakiś wykres, abo coś?

Nie.

> Bo
> jeśli mam za to zapłacić, to chcę znać ROI. Skoro te testy mają mieć
> efektywność probabilistyczną, to być może bardziej opłaca się
> wykupienie polisy ubezpieczeniowej? To wcale nie jest śmieszne
> pytanie.

Myślę, że nikt ci nie sprzeda takiej polisy.

>> w przeciwieństwie do niekompletnego dowodu, który jest czystym
>> marnotrawstwem.
>
> Więc róbmy dowód kompletny.

To jest ryzyko, bo może się okazać, że zanim skończysz dowodzić, skończą
się pieniądze albo program przestanie być potrzebny w takiej postaci.