> > To skąd wiedzą, że dobrze wyspecyfikowały? Mają przeczucie?
>
> Stąd, że się na tym znają.

Ale znają się na tym, co sami z tego rozumieją. A specyfikacja jest po to, żeby to
ich rozumienie przekazać innym (np. programistom). I teraz jest problem: skąd taka
osoba wie, że dobrze coś wyspecyfikowała, skoro jej rozumienie tematu jest niejawnie
uzupełnione posiadaną wiedzą, której nie wyspecyfikowała, ale tego nie zauważyła? To
jest powszechne zjawisko.

Metody formalne przydają się też w tym, że pokazują luki w specyfikacji. Nawet w
czymś, co jest "oczywiste", ale przestaje być oczywiste, jak automat wypunktuje
niejawnie pominięte założenia.

> W praktyce funkcję sort pisze się bardzo rzadko.

W praktyce każdą rzecz pisze się jeszcze rzadziej. Tym bardziej nie ma pewności, czy
wszyscy wszystko tak samo dobrze rozumieją.

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

Czyli biznes typu "wicie rozumicie". Jedna wielka szara strefa.
Na budowie desek ma być tyle, żeby się nie zawaliło. Czy może być jedna mniej, niż
ostatnio? Nie wiemy, bo w praktyce niczego nie mierzymy i nie wiemy, gdzie jesteśmy z
parametrami.

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

Tak. Ale skoro już zarabiają, to nie poprzestajmy na tym, tylko optymalizujmy. Może
mogłyby zarabiać więcej? Problem w tym, że bez dokładnej wiedzy o tym co uzyskaliśmy,
nie wiadomo, co i jak zmienić.

W porównaniu do innych branż inżynierskich, my jesteśmy w głębokim lesie.

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

To oczywiście będzie zależało od wielu parametrów, w szczególności od tego, jaki jest
koszt fakapu. Zwykle jest bardzo mały, więc jedyna rzecz, która jest faktycznie
opłacalna, to klepanie kodu.

> 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 nie chodzi o to, żeby za każdym razem wynajdywać nowe metody. Nie wynajdujemy
nowego języka programowania do każdego projektu. Jest pula rozwiązań i metod, z
których korzystamy w razie potrzeby.

> Instytucje finansowe zajmują się zarabianiem pieniędzy

Wszyscy sie tym zajmują. Nie napinajmy się, że instytucje finansowe niby mają jedną
nóżkę bardziej.

> A straty z błędów są
> jak najbardziej realne,

Nie będę wybiegał poza tematykę grupy zagłębiając się w tą część wątku, bo na pewno
bym wybiegł za daleko.

> 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.

W systemie finansowym? Zrobiłbym go dokładnie takimi metodami, jakie opisałeś. Byłoby
to w zgodzie z:

1. potencjalnymi kosekwencjami dla mnie w przypadku fakapu
2. potencjalnymi korzyściami, np. w postaci wysokich premii
3. mojej osobistej opinii nt. realności strat w tym systemie

Serio. Ja też umiem liczyć.

A teraz porozmawiajmy o pociągach. Albo windach. Albo sprzęcie medycznym. Albo o
samochodach, to teraz dosyć popularny temat. Albo o czymkolwiek innym, gdzie, jak to
mówi przysłowie, programista wiesza się razem ze swoim programem, zwłaszcza gdy sam
staje się jego użytkownikiem.

> 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.

Bo nie musi tak być.

> > 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.

A ja myślę, że takie polisy będą. Razem z całym systemem wyliczania ich wysokości.

> > 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.

Widziałem też przypadek, kiedy skończyły się pieniądze na testy.

--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com