W dniu sobota, 28 marca 2015 10:10:20 UTC+1 użytkownik Maciej Sobczak napisał:
> > w przeciwieństwie do niekompletnego dowodu, który jest
> > czystym marnotrawstwem.

istotnie, rozumowanie albo czegoś dowodzi (i wtedy jest dowodem), albo
nie dowodzi (i wtedy nie jest dowodem; wtedy może najwyżej być próbą
perswazji)

jakoś nie umiem w swojej głowie oddzielić znaczeń sformułowań "niekompletny
dowód" od "test", tak jak nie umiem oddzielić znaczeń sformułowań
"kompletny test" od "dowód" (może w tym ostatnim przypadku można powiedzieć,
że "kompletny test" jest jednym z możliwych rodzajów dowodu -- poprzez
indukcję enumeracyjną; z drugiej strony, choć testy można widzieć jako
szczególny przypadek niekompletnego dowodu, to pewnie ogólniejszym
znaczeniem sformułowania "niekompletny dowód" jest "rozumowaniem o strukturze
dowodu, w którym występują luki", tzn. np. korzysta z jakichś wątpliwych
lematów)

do góry

On Saturday, March 28, 2015 at 9:45:23 AM UTC+1, g...@g...com wrote:
> W dniu sobota, 28 marca 2015 05:04:04 UTC+1 użytkownik M.M. napisał:
>
> > > W takim razie zgoda -- tego rodzaju "poprawność" jest niemożliwa do uzyskania.
> > > Należy jednak mieć na uwadze, że z formalnego punktu widzenia poprzez
> > > "poprawność" dowodu rozumie się to, czy każdy krok jest zgodny z regułami,
> > > natomiast w tym przypadku raczej należałoby użyć słowa "adekwatność"
> > > (na przykład teza Churcha-Turinga postuluje adekwatność maszyny Turinga
> > > jako modelu ujmującego intuicyjne rozumienie obliczalności)
> >
> > Mój (hipotetyczny) klient zamawia najlepszy program do gry w
> > szachy o łącznym rozmiarze kodu i danych nie większym niż 1MB. Napisałem
> > taki program. Jak mam przeprowadzić dowód, że nie istnieje w
> > ramach tego rozmiaru lepszy program?
>
> To akurat nie jest problem metody dowodowej,
Właśnie, tego nie da się udowodnić, a jest to też ważny aspekt
programu. A w testach tak się robi, porównuje się kilka
różnych algorytmów dla różnych danych.

> tylko nieprecyzyjnej
> specyfikacji. Co to znaczy,że "w ramach określonego rozmiaru program
> jest lepszy od innego programu"?
Zakładamy że specyfikacja jest dobra. To jest kwestia jakości
użytych algorytmów/heurystyk.


> Zresztą cechy użytkowe nie są czymś, co dowodzi się formalnie
> (bo są subiektywne). Formalnie chcemy dowodzić raczej pewnych
> inwariantów -- że na przykład w programie wielowątkowym nie dojdzie
> do sytuacji dead-locku (klasyczne zastosowane logik temporalnych),
Nie słyszałem o logice temporalnej. Może się mylę, ale to się
wydaje łatwe. Dla mnie taki dowód sprowadza się do tego, aby
wszystkie pary kodu, który może wykonać się równolegle, były
opatrzone semaforami w tej samej kolejności w sensie wykonania i
w odwrotnej kolejności (też w sensie wykonania).


> że dla określonej klasy danych wejściowych program się zatrzyma,
> że zużycie zasobów w czasie działania programu będzie ograniczona
> określoną funkcją od czasu działania i rozmiaru danych wejściowych
> itd.
To czasami może być trudne, np. problem Collatza. Pytanie czy
czas wykonania i inne zasoby są znanymi/łatwymi funkcjami danych
wejściowych. Jeśli zapotrzebowanie na zasoby w danym programie
nawet da się rozbić na wiele małych-łatwych funkcji, to może
potem wyjść: f1(N) * f2(N) * f3(N) * f4(N) * f5(N). Można
wziąć maksimum każdej z tych pięciu funkcji i podać, jako oszacowanie
górne, iloczyn maksimów. Ale w praktyce oszacowanie górne
może nie mieć nic wspólnego z rzeczywistością, gdy f1
przyjmuje maksimum, to pozostałe funkcje mogą przyjmować
małe wartości. Zależności fi od fj (i!=j) może być bardzo
skomplikowana...

Pozdrawiam

do góry

On Saturday, March 28, 2015 at 10:48:17 AM UTC+1, g...@g...com wrote:
> W dniu sobota, 28 marca 2015 10:10:20 UTC+1 użytkownik Maciej Sobczak napisał:
> > > w przeciwieństwie do niekompletnego dowodu, który jest
> > > czystym marnotrawstwem.
>
> istotnie, rozumowanie albo czegoś dowodzi (i wtedy jest dowodem), albo
> nie dowodzi (i wtedy nie jest dowodem; wtedy może najwyżej być próbą
> perswazji)
>
> jakoś nie umiem w swojej głowie oddzielić znaczeń sformułowań "niekompletny
> dowód" od "test", tak jak nie umiem oddzielić znaczeń sformułowań
> "kompletny test" od "dowód"
Bo z punktu widzenia praktycznych korzyści (gdy już mamy
jedno albo drugie!) nie ma najmniejszej różnicy. Różnice mogą
się pojawiać w nakładzie pracy. Raz może być łatwiejsze przeprowadzenie
dowodu, drugi raz napisanie testów.

> (może w tym ostatnim przypadku można powiedzieć,
> że "kompletny test" jest jednym z możliwych rodzajów dowodu -- poprzez
> indukcję enumeracyjną;
Nawet w niekompletnym teście, prawdopodobieństwo błędu maleje jak w
paradoksie dnia urodzin, myślę, że wystarczająco szybko dla
praktycznych zastosowań. Oczywiście trzeba zapewnić aby dane wejściowe
miały równomierny rozkład (albo lepszy dla danego zadania) no i trzeba
te testy napisać, najlepiej bezbłędnie. W trakcie testowania, kod
testowany niby staje się automatycznie kodem testowym i na odwrót, ale
problem w tym, że mogą być identyczne błędy w obu kodach.


> z drugiej strony, choć testy można widzieć jako
> szczególny przypadek niekompletnego dowodu, to pewnie ogólniejszym
> znaczeniem sformułowania "niekompletny dowód" jest "rozumowaniem o strukturze
> dowodu, w którym występują luki", tzn. np. korzysta z jakichś wątpliwych
> lematów)
Nie rozumiem.

Pozdrawiam

do góry

On 28/03/2015 10:47, g...@g...com wrote:
> W dniu sobota, 28 marca 2015 10:10:20 UTC+1 użytkownik Maciej Sobczak napisał:
>>> w przeciwieństwie do niekompletnego dowodu, który jest
>>> czystym marnotrawstwem.
>
> istotnie, rozumowanie albo czegoś dowodzi (i wtedy jest dowodem), albo
> nie dowodzi (i wtedy nie jest dowodem; wtedy może najwyżej być próbą
> perswazji)
>
> jakoś nie umiem w swojej głowie oddzielić znaczeń sformułowań "niekompletny
> dowód" od "test",

Przez "niekompletny dowód" miałem na myśli to, co się ma pomiędzy
rozpoczęciem przeprowadzania formalnego dowodu, a zakończeniem go. Jeśli
zacząłeś dowodzić w poniedziałek i skończyłeś w piątek, to to co miałeś
w środę to był niekompletny dowód.

do góry

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.

do góry

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

do góry

On Thu, 26 Mar 2015 07:03:06 -0700 (PDT), Maciej Sobczak
<s...@g...com> wrote:
> W finansach nie ma strat. Albo się "traci" coś, czego nigdy nie
było =
> (wtedy nie ma strat), albo można to stosunkowo łatwo odkręcić przez=
> reklamacje i wtedy (relatywnie) też nie ma strat.

Bzdury.

> Masz rację, że w finansach nie stosuje się dowodów ale nie dlatego,=
> że są droższe od testów, tylko dlatego, że testów też się =
> tam nie robi.

Bzdury.

RW

do góry

On Fri, 27 Mar 2015 02:06:10 -0700 (PDT), Maciej Sobczak
<s...@g...com> wrote:
> 1. Czy ktoś poniósł kiedyś osobiste konsekwencje (np. poszedł do =
> pierdla) za zrobienie błędu w programie użytym w branży finansowej?

Ludzie tracili posady. Do więzienia programistów nie wsadza się w
żadnej branży.

> 2. Czy ktoś odniósł kiedyś osobiste korzyści (np. dostał wysok=
> ą premię) za szybkie wdrożenie systemu na rynek, wyprzedzając tym k=
> onkurencję?

Owszem.

RW

do góry

On Sat, 28 Mar 2015 18:43:10 +0000, Roman W
<b...@g...pl> wrote:

>On Fri, 27 Mar 2015 02:06:10 -0700 (PDT), Maciej Sobczak
><s...@g...com> wrote:
>> 1. Czy ktoś poniósł kiedyś osobiste konsekwencje (np. poszedł do =
>> pierdla) za zrobienie błędu w programie użytym w branży finansowej?
>
>Ludzie tracili posady. Do więzienia programistów nie wsadza się w
>żadnej branży.
>
>> 2. Czy ktoś odniósł kiedyś osobiste korzyści (np. dostał wysok=
>> ą premię) za szybkie wdrożenie systemu na rynek, wyprzedzając tym k=
>> onkurencję?
>
>Owszem.
>
>RW

Popieram

A.L.

do góry

On Sat, 28 Mar 2015 18:38:44 +0000, Roman W
<b...@g...pl> wrote:

>On Thu, 26 Mar 2015 07:03:06 -0700 (PDT), Maciej Sobczak
><s...@g...com> wrote:
>> W finansach nie ma strat. Albo się "traci" coś, czego nigdy nie
>było =
>> (wtedy nie ma strat), albo można to stosunkowo łatwo odkręcić przez=
>> reklamacje i wtedy (relatywnie) też nie ma strat.
>
>Bzdury.
>
>> Masz rację, że w finansach nie stosuje się dowodów ale nie dlatego,=
>> że są droższe od testów, tylko dlatego, że testów też się =
>> tam nie robi.
>
>Bzdury.
>
>RW

Nareszcie glos rozsadku. Smaic mi sie chce ze "specjalistow"
wypowiadajacych sie w tym watku.

A.L.

do góry