Użytkownik napisał w wiadomości grup
dyskusyjnych:a8e9d2c8-3f9c-4256-aabc-1447655cd1fe@go
oglegroups.com...

>Jeżeli idzie o mnie, to nie, nie próbowałem nawet nigdy zrobić systemu
>klasy A według Orange Book DoD.

Ale - pewnie z tego jesteś dumny - doskonale zdajesz sobie sprawę że w/w OS
klasy A byłby właśnie tym, co najbardziej byłoby potrzebne... inne
popierdułki mogą poczekać.

Czyli, rozumując rozumnie, skoro nie udało się to tam gdzie najbardziej była
tego potrzeba - to co się udało? Pochwal się. Przecież jesteś taki bystry i
masz mnóstwo doświadczenia w temacie, którym możesz się z nami podzielić.

do góry

W dniu wtorek, 31 marca 2015 23:04:58 UTC+2 użytkownik slawek napisał:
> Użytkownik napisał w wiadomości grup
> dyskusyjnych:a8e9d2c8-3f9c-4256-aabc-1447655cd1fe@go
oglegroups.com...
>
> >Jeżeli idzie o mnie, to nie, nie próbowałem nawet nigdy zrobić systemu
> >klasy A według Orange Book DoD.
>
> Ale - pewnie z tego jesteś dumny - doskonale zdajesz sobie sprawę że w/w OS
> klasy A byłby właśnie tym, co najbardziej byłoby potrzebne... inne
> popierdułki mogą poczekać.

Potrzebne komu do czego?

> Czyli, rozumując rozumnie, skoro nie udało się to tam gdzie najbardziej była
> tego potrzeba - to co się udało? Pochwal się. Przecież jesteś taki bystry i
> masz mnóstwo doświadczenia w temacie, którym możesz się z nami podzielić.

Nie twierdzę, że jestem bystry, jak również nie twierdziłem nigdzie,
że mam w temacie mnóstwo doświadczenia. Moje doświadczenie jest raczej
skromne, ale za to dzielę się nim chętnie, w związku z czym większość
swoich kart zdążyłem już tutaj wyłożyć.

Za to Twoje doświadczenie owiane jest mgłą tajemnicy, podtrzymywaną
dodatkowo przez konsekwentne wymigiwanie się od odpowiadania na pytania
oraz formułowanie lakonicznych i pogardliwych komentarzy, z których nic
nie wynika.

do góry

On 31/03/2015 09:56, Maciej Sobczak wrote:
> W dniu poniedziałek, 30 marca 2015 20:08:40 UTC+2 użytkownik Andrzej
> Jarzabek napisał:
>
> Nic nie szkodzi. Ja w swoim portfelu inwestycyjnym mam podobną ilość
> udziałów różnych firm inwestycyjnych właśnie po to, żeby strata Rysia
> i zysk Krzysia nie były problemem, tylko co najwyżej zmianą
> proporcji. Zdaje się, że taka dywersyfikacja inwestycyjna jest
> powszechną praktyką. Ot i cały dramat.

To nie do końca tak działa. Inwestorzy starają się mieć więcej udziałów
w tych firmach, co do których mają przypuszczenia, że więcej zarobią lub
jest niższe ryzyko straty. Jeśli są tacy, którzy oszacują to prawidłowo,
to kasa płynie do ich portfeli z portfeli tych, którzy źle zgadują lub w
ogóle nie biorą tego pod uwagę i kupują np. po równo.

Dalej - istnieją również firmy, które w ogóle nie są spółkami giełdowymi
i ich akcji nie da się kupić. Część z nich realizuje właśnie biznes plan
taki, że jakaś innowacyjna idea pozwoli im zarabiać kosztem bardziej
konserwatywnych korporacji.

>> Myślisz, że gdyby taka Toyota
>
> Zginęli ludzie. Nie rozmawiamy o kupowaniu akcji, tylko o tworzeniu
> poprawnego oprogramowania.

Bo przecież taki prezes firmy motoryzacyjnej chętnie zrezygnuje z premii
z zamian za spokojny sen, prawda?

>> A na rozbijających się samochodach Toyoty zyskuje Ford
>
> Nie. Ford robi w gacie, bo przecież do tej pory używał dokładnie
> takich samych metod, więc przypuszczalnie mają takie same problemy.

Ale przecież ludzie nie przestaną kupować samochodów, więc jak nie kupią
Toyoty, to kupią Forda.

> Dokładnie o tym piszę od samego początku. O rosnącym
> zainteresowaniu.
>
> Tzn. w pewnych branżach zainteresowanie rośnie a w innych nie
> rośnie.

Też pisałem od początku - są takie nisze, w których to ma sens.

>> Nie zgodzę się, jak najbardziej jest presja na szukanie lepszych
>> rozwiązań i wdrażanie nowych metod. Tylko że nie ma za bardzo
>> przesłanek na to, że metody formalne są lepszym rozwiązaniem.
>
> Najwyraźniej nie ma takiej potrzeby, albo się to nie kalkuluje. Od
> początku się w tym temacie zgadzamy.

Ja zrozumiałem twoją tezę tak, że niezależnie od potrzeby nikt tego nie
robi, bo straty nie są problemem.

>> No to ja przecież od początku chciałem się dowiedzieć, jak to
>> mogłoby wyglądać od strony praktycznej, a ty mnie zbyłeś mnie
>> opowieścią o tablicach i flamastrach.
>
> Nie. Napisałem wyraźnie, że zrobiłbym to dokładnie tak, jak opisałeś.
> Bo ja też umiem liczyć.

Bo byś kalkulował co najlepsze dla ciebie jako pracownika etatowego, czy
również dlatego, że jako profesjonalista podejmowałbyś decyzje twoim
zdaniem najlepsze dla firmy? Korzystając z komfortu braku konieczności
wybierania między maksymalizacją zysku a minimalizacją ilości trupów...

do góry

Użytkownik napisał w wiadomości grup
dyskusyjnych:01625116-4980-43e6-91e8-873f3e991d3c@go
oglegroups.com...

>Potrzebne komu do czego?

A zapodaną Orange Book czytał? Nie czytał? To dlaczego się dziwi, że nie wie
do czego i komu potrzebne?

>Nie twierdzę, że jestem bystry, jak również nie twierdziłem nigdzie,
>że mam w temacie mnóstwo doświadczenia. Moje doświadczenie jest raczej
>skromne, ale za to dzielę się nim chętnie, w związku z czym większość

Więc się podziel. Gdzie i do czego? Przecież skoro uważasz, ze dowody
formalne to podstawa, to chyba nie konfabulujesz, tylko opierasz się na
faktach.

do góry

W dniu wtorek, 31 marca 2015 23:59:41 UTC+2 użytkownik slawek napisał:

> >Nie twierdzę, że jestem bystry, jak również nie twierdziłem nigdzie,
> >że mam w temacie mnóstwo doświadczenia. Moje doświadczenie jest raczej
> >skromne, ale za to dzielę się nim chętnie, w związku z czym większość
>
> Więc się podziel.

Przecież się podzieliłem. Wszystko, o czym piszę, staram się
dokumentować, podawać odnośniki. Jeżeli masz jakieś konkretne
pytanie, to je zadaj, a wówczas postaram się odpowiedzieć
w miarę swoich skromnych możliwości

> Gdzie i do czego? Przecież skoro uważasz, ze dowody
> formalne to podstawa, to chyba nie konfabulujesz, tylko opierasz się na
> faktach.

Gdzie napisałem, że "dowody formalne to podstawa"? Podstawa czego?

do góry

W dniu poniedziałek, 30 marca 2015 10:25:57 UTC+2 użytkownik firr napisał:
> W dniu piątek, 27 marca 2015 10:57:26 UTC+1 użytkownik g...@g...com napisał:
> > > Myślę że w praktyce w ogóle nie ma możliwości przeprowadzenia takiego
> > > dowodu, nawet dla mniejszych programów. Jak udowodnić, że w dowodzie
> > > nie ma błędu?
> >
> > To jest akurat rzecz podstawowa: wystarczy pokazać, że każdy krok dowodu
> > wynika logicznie z tez dowiedzionych wcześniej, albo przyjętych przez nas
> > aksjomatów, w oparciu o uznawane przez nas reguły wnioskowania
> > (które uważamy za oczywiste).
> >
>
> nie jestem pewien czy to wystarczy.. czasem moze nawet dosyc czesto moze okazac sie
ze
> mio ze te wnioskowania byly poprawne to
> ogolnie problem wynika z przeoczenia pewnych
> pobocznych czynników
>
> innymi slowy mi wyglada na to ze dowody sa
> rowniez czesciowe tak samo jak testy ;/
>

wogole chyba mozna powiedziec ze dowodzeniu i testowaniu mozna przyznac 'moralny'
remis

do góry

W dniu środa, 1 kwietnia 2015 00:08:38 UTC+2 użytkownik g...@g...com napisał:
> W dniu wtorek, 31 marca 2015 23:59:41 UTC+2 użytkownik slawek napisał:
>
> > >Nie twierdzę, że jestem bystry, jak również nie twierdziłem nigdzie,
> > >że mam w temacie mnóstwo doświadczenia. Moje doświadczenie jest raczej
> > >skromne, ale za to dzielę się nim chętnie, w związku z czym większość
> >
> > Więc się podziel.
>
> Przecież się podzieliłem. Wszystko, o czym piszę, staram się
> dokumentować, podawać odnośniki. Jeżeli masz jakieś konkretne
> pytanie, to je zadaj, a wówczas postaram się odpowiedzieć
> w miarę swoich skromnych możliwości
>
> > Gdzie i do czego? Przecież skoro uważasz, ze dowody
> > formalne to podstawa, to chyba nie konfabulujesz, tylko opierasz się na
> > faktach.
>
> Gdzie napisałem, że "dowody formalne to podstawa"? Podstawa czego?

dowodzenie to tak naprawde postawa kodowania
- programujac bez przerwy dowodzisz sobie
ze piszac A a pozniej B wynik bedzie taki jak
zalożony
sa to nawet mz zupelnie formalne dowodzenia

gorzej jest jesli ktos pracuje gdzies w jakiejs
firmie np pod presja czasu i nie jest do konca
pewien jak działa np jakies api z ktorym sie
łaczy wtedy ten łancuch dowodzenia moze sie
zerwać (mnie np mozno irytowaly moje pierwsze
doswiadczenia a winapi ktore mz nie bylo w tym
sensie odpowiednio udokumentowane tak ze mozna
co najwyzej prawdopodobnie zalozyc a nie
miec pewnosc ze ten kod jest ok - (pozniej mi
troche minelo posrednio na skutek powtarzalnosci
testowania i posrednio tez na skutek ogladania
innych kodów ktore maja to zrobione tak samo)

do góry

On Tuesday, March 31, 2015 at 7:49:55 PM UTC+2, g...@g...com wrote:
> W dniu wtorek, 31 marca 2015 19:29:20 UTC+2 użytkownik M.M. napisał:
> > >
> > > "Najlepiej jak to możliwe" -- to też nieprecyzyjne określenie.
> > > Można je rozumieć jako "najlepiej jak komputer potrafi", albo
> > > "najlepiej jak programista potrafi". To ostatnie jest zresztą
> > > zazwyczaj twardym limitem, chyba że klient znajdzie lepszego
> > > programistę
> > No oczywiście że jest nieprecyzyjne. Jest nieprecyzyjne jak każde
> > generalizowanie.
>
> Generalizowanie to tyle, co uogólnianie, czyli przechodzenie
> od przypadku konkretniejszego do ogólniejszego. Stąd, że Twoje
> generalizowanie jest nieprecyzyjne, nie wynika, że każde generalizowanie
> jest nieprecyzyjne.
Poczekaj bo się robią jakieś jaja z tej rozmowy:) Wątek ten dotyczy (nie)przydatności
formalnego dowodu na poprawność programu w
praktyce programistycznej/biznesowej. Potem ja wtrąciłem, że
wymagania są różne, np. klient chce najlepszy program. Jak słuszne
zauważyłeś, nie precyzowałem co oznacza najlepszy. Piłem do tego,
że jeśli już tak ściśle i formalnie chcemy dowodzić, to należało
by również dowieść, że program istotnie jest najlepszy. Więc moje
generalizowanie obejmuje zbiór kryteriów według których
w praktyce programistycznej ocenia się programy. Co widzisz
nieprecyzyjnego w takim generalizowaniu? Albo jakie kryteria
uznajesz (we wcześniejszym poście) za łatwe. Mój klient np.
chce, aby program zarobił jak najwięcej pieniędzy i wymagał
jak najmniejszego personelu do jego administracji. Takie
stawia wymagania. A czy mu dostarczę program do grania na
giełdzie, czy serwis do ogłoszeń matrymonialnych to sprawa
drugorzędna.


> Na przykład dodanie funkcji porównującej jako parametru
> dla funkcji "sort" jest generalizowaniem, a jest piekielnie
> precyzyjne.
Dlaczego można precyzyjne generalizować po tejże funkcji, a po
spotykanych kryteriach oceny programu nie można?

>
> > > Powiedzieć, że coś "działa jak najlepiej", to coś innego, niż
> > > powiedzieć, że "nie istnieje w ramach pewnych ograniczeń lepszy program"
> > > (nie jest nawet jasne, co się tutaj rozumie w kwestii "istnienia programu"
> > > -- czy chodzi o jakiś program dostępny na rynku, czy taki, który
> > > ktoś potencjalnie mógłby napisać)
> > Przypuszczasz, że chodziło mi o dowód formalny (na podstawie kodu
> > źródłowego) na istnienie lepszego programu na rynku? ;-)
>
> Problem polega na tym, że nie wiem, o co Ci chodziło, bo wyraziłeś
> się dość nieprecyzyjnie
Myślałem że jak tylko odrzucisz przypadki nonsensowne, to będzie
precyzyjnie.

>
> > > > Inny przykład, program do translacji języków naturalnych. Dlaczego
> > > > chciałbyś używać gorszy program niż lepszy?
> > >
> > > Ja nie wiem, co to znaczy w tym kontekście "gorszy", a co "lepszy"
> > A ja wiem że wiesz, potrafisz odróżnić tekst dobrze przetłumaczony od
> > źle przetłumaczonego.
>
> W pewnym zakresie może tak. Ale znajdzie się również taki, w którym
> eksperci będą między sobą dywagować, czy Słomczyński, czy Barańczak
TO też da się rozwiązać, można uznać za takie same, jeśli eksperci od
razu nie są jednoznaczni - ale nie ma sensu brnąć dalej.

>
> > > Oczywiście, kiedy masz już pewne kryterium jakości, to możesz się
> > > pokusić o przeprowadzenie formalnego dowodu w odniesieniu do tego
> > > kryterium
> > Nie wiem jak można udowodnić na podstawie źródeł dwóch
> > programów, który program lepiej tłumaczy tekst.
>
> Też nie wiem. Prawdopodobnie nie można, tym bardziej, że
> nie umiemy nawet uściślić, co to znaczy "lepiej tłumaczyć tekst"
No więc właśnie. Co z tego, że nawet jeśli są jakieś znikome
szanse na udowodnienie poprawności programu, to zwykle nie ma
żadnych szans, czy program, choć jest poprawny, to realizuje
zamierzony cel.


> > > Przeciwnie. Dla pewnych kryteriów przeprowadzenie formalnych dowodów
> > > będzie prostsze, dla innych trudniejsze, a dla jeszcze innych niemożliwe.
> > Różnych programów o rozmiarze N bajtów mamy 256^N. Mamy definicję
> > dopuszczalnych danych wejściowych, być może wraz z rozkładem
> > prawdopodobieństwa. Mamy precyzyjnie określone co oznacza najlepszy.
> > Jak udowodnić, że wśród 256^N nie istnieje żaden lepszy program
> > od naszego?
>
> W niektórych przypadkach możemy być może policzyć, jaka jest teoretyczna
> granica wydajności, i pokazać, że nasz algorytm ją realizuje (jeżeli
> poprze "lepszość" rozumiemy mniejszą złożoność obliczeniową)
Nie wiem czy jest to możliwe. Dla mnożenia macierzy kwadratowych wszyscy
byli przekonani że dolna granica to N^3 - a okazało się że nie.


> Ale niestety Twoje użycie słowa "najlepszy" jest nieprecyzyjne,
> bo "najlepszy" może być również w sensie "maintainability" -- że
> ma najlepsze komentarze, jest najłatwiej rozszerzalny itd.
Oczywiście że może. Przecież to jest bardzo często spotykany
wymóg. Ja np. mam sprzeczne wymogi: program ma być wydajny, ma
obsługiwać bardzo dużą ilość użytkowników na tanim sprzęcie i
jednocześnie ma być bardzo podatny na zmiany, żeby szybko go
rozbudowywać.



> > > Nieprawda. To, jak się coś skonkretyzuje (oraz co się skonkretyzuje),
> > > ma kluczowe znaczenie dla łatwości/trudności przeprowadzenia dowodu.
> > Może czegoś nie wiem, dla jakich kryteriów dowód będzie łatwy w
> > przeprowadzeniu?
>
> Nie rozumiem o co pytasz. W ogólności zależy to od przypadku.
Pytam o to, jakie miałeś na myśli przypadki, gdy pisałeś, że
może dowód być łatwy.

>
> > > > > Mylisz się z pewnością, choćby dlatego, że semafor nie jest jedynym
> > > > > mechanizmem synchronizującym używanym w programach wielowątkowych.
> > > > Jeśli odebrałeś moje słowa dosłownie, to mam prośbę. Najpierw uogólnij
> > > > sobie mój 'semafor' na inne mechanizmy synchronizowania, a potem
> > > > przeanalizuj czy się mylę. Potem pogadamy dalej.
> > >
> > > Na przykład w API CUDA dla GPU nVidii masz polecenie __syncthreads(), które
> > > działa w taki sposób, że wszystkie wątki czekają, aż ostatni wątek wywoła
> > > owo polecenie. Deadlocka otrzymamy w każdym przypadku, gdy którykolwiek
> > > z wątków w danej jednostce uruchomieniowej nie wywoła polecenia
__syncthreads().
> > Nigdy nie używałem tego polecenia. Czy jest konieczne używanie?
> > Co ono usprawnia?
>
> Umożliwia synchronizację wątków przed dostępem do pamięci.
Po to jest prawie każda synchronizacja, a jeśli słowo pamięć
zmienimy na zasób, to chyba dosłownie każda.

> Jeśli Cię to bardziej interesuje, polecam kurs z "Heterogenous Parallel
> Programming" na Courserze albo książkę "CUDA w przykładach" (wyd. Helion)
Nie mam aż tyle czasu, myślalem że rzucisz kilka zalet.

>
> > > W jaki sposób przetłumaczyłbyś tę sytuację na swój "ogólniony semafor"?
> > Nie wiem, w taki sposób nie programowalem nigdy. Na pewno wszystkie
> > wątki muszą dojść do tej instrukcji. A żeby doszły, to nie mogą się
> > wcześniej zablokować i syncthreads musi być wspólną instrukcją....
> >
> > Chyba mam sposób. Jeśli używam N semaforów s1, s2, ... sN, to zakładam, że
> > każde synthreads jest objęte:
> > s1
> > s2
> > sn
> > syncthreds
> > sn
> > s2
> > s1
> > Potem używam wszędzie w tej samej kolejności od s1 do sn.
>
> Nie. Każdy wątek może bezpiecznie wywołać __syncthreads i nie ma potrzeby
> zabezpieczania jej semaforami,
Nie pisałem że trzeba ją zabezpieczać semaformai, tylko że trzeba ją
traktować jakby była zabezpieczona według takiego schematu.

> zaś (pomijając kwestię marnowania zasobów)
> właśnie z tego względu zabezpieczanie semaforami nic w tym przypadku nie
> da, a tym bardziej nie ochroni przed deadlockiem.
Nie wiem totalnie o co chodzi. Semafory nigdy nie chronią przed deadlockiem,
chroni właściwa metoda używania semaforów.

Pozdrawiam

do góry

On Wednesday, April 1, 2015 at 9:01:27 AM UTC+2, firr wrote:
> W dniu środa, 1 kwietnia 2015 00:08:38 UTC+2 użytkownik g...@g...com
napisał:
> > W dniu wtorek, 31 marca 2015 23:59:41 UTC+2 użytkownik slawek napisał:
> >
> > > >Nie twierdzę, że jestem bystry, jak również nie twierdziłem nigdzie,
> > > >że mam w temacie mnóstwo doświadczenia. Moje doświadczenie jest raczej
> > > >skromne, ale za to dzielę się nim chętnie, w związku z czym większość
> > >
> > > Więc się podziel.
> >
> > Przecież się podzieliłem. Wszystko, o czym piszę, staram się
> > dokumentować, podawać odnośniki. Jeżeli masz jakieś konkretne
> > pytanie, to je zadaj, a wówczas postaram się odpowiedzieć
> > w miarę swoich skromnych możliwości
> >
> > > Gdzie i do czego? Przecież skoro uważasz, ze dowody
> > > formalne to podstawa, to chyba nie konfabulujesz, tylko opierasz się na
> > > faktach.
> >
> > Gdzie napisałem, że "dowody formalne to podstawa"? Podstawa czego?
>
> dowodzenie to tak naprawde postawa kodowania
> - programujac bez przerwy dowodzisz sobie
> ze piszac A a pozniej B wynik bedzie taki jak
> zalożony
Zgadzam się, tyle że rzadko kto robi to formalnie. Ja przyznaję,
że już dawno w ogóle zapomniałem jak się formalnie przeprowadza
dowody. Może warto byłoby się podszkolić...


> sa to nawet mz zupelnie formalne dowodzenia
Właśnie tego nigdy u nikogo nie zaobserwowałem.


> gorzej jest jesli ktos pracuje gdzies w jakiejs
> firmie np pod presja czasu
Nie dość że pod presją czasu, to jeszcze pod innymi
presjami a do tego nie wie czy za chwile ktoś nie
zmieni zdania i duża część systemu nie pójdzie do
kosza.

> i nie jest do konca
> pewien jak działa np jakies api z ktorym sie
> łaczy wtedy ten łancuch dowodzenia moze sie
> zerwać
To już w ogóle robi się sieczka.

> (mnie np mozno irytowaly moje pierwsze
> doswiadczenia a winapi ktore mz nie bylo w tym
> sensie odpowiednio udokumentowane tak ze mozna
> co najwyzej prawdopodobnie zalozyc a nie
> miec pewnosc ze ten kod jest ok - (pozniej mi
> troche minelo posrednio na skutek powtarzalnosci
> testowania i posrednio tez na skutek ogladania
> innych kodów ktore maja to zrobione tak samo)

do góry

W dniu środa, 1 kwietnia 2015 12:03:58 UTC+2 użytkownik M.M. napisał:
>
> > gorzej jest jesli ktos pracuje gdzies w jakiejs
> > firmie np pod presja czasu
> Nie dość że pod presją czasu, to jeszcze pod innymi
> presjami

pod jakimi na przyklad*? ja np osobiscie nie na.leze do ludzi dla ktorych pracowanie
pod
presją daje dobre wyniki

* mi do glowy przychodzą
- rozpraszajacy ludzie
- rozpraszajace obowiazki poboczne
- newygoda siedzenie 8h na tylku
( - problemy zdrowotne (gorsze do ogarniecia w publicznej lokalizacji)

do góry