On 2015-09-12 12:18, AK wrote:
>
> PS: Moze i jest dzis w srodowisku C++ bardzo wielu dobrych w
> numeryce/algorytmice
> ludzi, ale _napewno_ Ty do nich nie nalezysz. nie masz
> _najmniejszego pojecia_
> o rzeczach ktore krytykujesz/dyskredytujesz.
>
Akurat Sebastian ma pojecie, zle trafiles. Zamiast sie zaperzac postaraj
sie zrozumiec co on pisze.

Pozdrawiam

Marek

do góry

Użytkownik "Waldek Hebisch" <a...@m...uni.wroc.pl> napisał:

> Z innej beczki, kilka lat temu zweryfikowano
> formalnie mikrojado L4.

Nie wierzę. C nie nadaje sie do weryfikacji formalnej poprawnosci programow
w nim pisanych (chyba ze jest to baaardzo okrojone C - i to o wiele bardziej niz
Misra C),
a jadro to jaderko na przyslowiowych "kilku kartkach" i "specjalnie pisane" pod
werfyfikację.

W zwyklym C/C++ formalna weryfikacja pooprawnosci to zwykla
uluda (i taka na zawsze zostanie).

AK


---
Ta wiadomość została sprawdzona na obecność wirusów przez oprogramowanie antywirusowe
Avast.
https://www.avast.com/antivirus

do góry

Użytkownik "Sebastian Biały" <h...@p...onet.pl> napisał:

>> A tak stalo sie z FreeBSD
>
> Serio? W moim internecie jeszcze jest:
>
> https://www.freebsd.org/

Ale u providerow juz prawie pełna plaża :)

> No proszę, ciach i mozna migrowac serwery z jednego niestabilnego środowiska w inne
niestabilne
> środowisko.

E no :) To Gentoo jakos mi dziala (bo dbam o nie conieco, choc
jest to - jak to Linux- wk..co upierdliwe. Specjalnie wybralem wlasnie Gentoo:)

AK


---
Ta wiadomość została sprawdzona na obecność wirusów przez oprogramowanie antywirusowe
Avast.
https://www.avast.com/antivirus

do góry

Użytkownik "Marek Borowski" <m...@n...com> napisał:

> Akurat Sebastian ma pojecie, zle trafiles. Zamiast sie zaperzac postaraj sie
zrozumiec co on
> pisze.

80% z tego co pisze to totalne widzimisie.
Nie widze, aby mial pojecie chociaz troche zasłaniające zwykly fanatyzm :)
W/g nigo MS to syf, .NET to syf, Win syf , CADy to prymitywny rynkowy soft :)
Za to C++ uber alles. Super przenosny, super bezpieczny, super wydajny.
Sorry, ale to jest najzwyklejsza paranoja :)

AK


---
Ta wiadomość została sprawdzona na obecność wirusów przez oprogramowanie antywirusowe
Avast.
https://www.avast.com/antivirus

do góry

On 2015-09-13 22:01, AK wrote:
>>> A tak stalo sie z FreeBSD
>> Serio? W moim internecie jeszcze jest:
>> https://www.freebsd.org/
> Ale u providerow juz prawie pełna plaża :)

Nie rozumiem żartu, widocznie za młody jestem.

>> No proszę, ciach i mozna migrowac serwery z jednego niestabilnego
>> środowiska w inne niestabilne środowisko.
> E no :) To Gentoo jakos mi dziala

Super. To ostateczny dowód.

do góry

On 2015-09-13 22:07, AK wrote:
> W/g nigo MS to syf

Nie.

>, .NET to syf

Nie.

> , Win syf

Nie.

> , CADy to prymitywny rynkowy
> soft :)

Nie.

> Za to C++ uber alles

Nie.

>. Super przenosny, super bezpieczny, super wydajny.

Nie.

Czyli 6:0 dla Ciebie. Tak dzialają newsy na advocacy. Chociaz czekaj, tu
nie jest advocacy...

do góry

On Sat, 12 Sep 2015 19:26:50 +0200, "AK" <n...@n...com> wrote:
> PS: Co do Pythona. Dlaczego "nie daj Boze?". Numpy czy Scipy
> pythonowe sa juz calkiem ok (polecam jeszcze numexpr - w
duzym
> stopniu neutralizuje problem z pythonowym GIL).

Pod warunkiem, że się nie używa dat. W Pythonie sa co najmniej trzy
klasy do dat: datetime.datetime, numpy.datetime64 i pandas.Timestamp.
Aha, i geniusze którzy projektowali datetime zapomnieli, że ktoś może
mieć timestamps z nanosekundami " bo przecież żaden zegar w pececie
nie ma takiej rozdzielczości " :)

RW

do góry

AK <n...@n...com> wrote:
> U?ytkownik "Waldek Hebisch" <a...@m...uni.wroc.pl> napisa?:
>
> > Z innej beczki, kilka lat temu zweryfikowano
> > formalnie mikrojado L4.
>
> Nie wierz?. C nie nadaje sie do weryfikacji formalnej poprawnosci programow
> w nim pisanych (chyba ze jest to baaardzo okrojone C - i to o wiele bardziej niz
Misra C),
> a jadro to jaderko na przyslowiowych "kilku kartkach" i "specjalnie pisane" pod
werfyfikacj?.
>
> W zwyklym C/C++ formalna weryfikacja pooprawnosci to zwykla
> uluda (i taka na zawsze zostanie).
>

Mikrojado L4 ma kolo 8000 lini kodu. Sa ograniczenia na to co sie
weryfikuje i na jezyk. ZCW weryfikacja obemuje np. sprawdzenie ze
nie ma przepelnien buforow. We efekci dostajesz z szukoscia
oczekiwana od C i najlepszym bezpieczenstwem jakie dzis daje
jakakolwiek techmika programowa. Kod L4 jest dostepny na sieci.
Za dokumentacje weryfikacji trzeba zaplacic grupa forse, wiec
ta czesc musisz przyjac na wiare,

A propo, Microsoft twierdzi ze maja lepsze metody i potrafia
zweryfikowac wieksze programy. Do calego Windowsa to daleko
(trzeba by milony linii), ale chca zwerufikwac kawalek
majacy kolo 60 tys. linii. Ostatnia wiadomosc jaka slyszalem
(rok czy dwa lata temu) ze zweryfkowali kolo 30 tys. linii.
Kod byl wczesnij napisany i ponoc jak sie cos nie chce
werifikowac to w kodzie poprawiaja tylko bugi, a przeciwnym
razie poprawija narzedzia.

Co do C to jest rozpracowana odpowiednia logika i ponoc teraz
nie sprawia wiecej problemow niz inne jezyki. Zeby bylo
jasne, weryfikcja polega na dodaniu (recznym) annotacji
i potem poprawnosc logiczna calosci sprawdza maszyna.
L4 wymagal cos kolo 8 linii annotacji na linie kodu.
Microsoft twierdzi ze przy ich metodzie wystarcza
kolo 1 lini annotacji na linie kodu. Na razie pisanie
annotacji wymaga duzo pracy i potrzeba do tego
kwalifikacji. Nie zmienia to faktu ze w przeszlosci
w mozna bylo tylko marzyc o weryfikacji na taka
skale.

Jesli interesuje Cie weryfikacja to mozesz popatrzyc na
pojekt CompCert:

compcert.inria.fr

Tam bierze sie normalny komilator C i weryfikje sie ze
kod maszynowy jest poprawnym tlumaczeniem zrodla.


--
Waldek Hebisch
h...@m...uni.wroc.pl

do góry

AK <n...@n...com> wrote:
> U?ytkownik "Waldek Hebisch" <a...@m...uni.wroc.pl> napisa?:
>
> > DO AK: Odra 1200 to polska konstrukcja.
>
> Odra1204. To prawda. To czysto polska konstrukcja.
>
> > Odry 1300 to i licencja od brytyjczykow.
>
> Bzdury Wasc pleciesz.
> To tez polska konstrukcja.
> Nie calkiem czysto polska, ale tez zadna licencja.
> Zaprojektowana i wykonana od 0 przez Polske/Polakow (z duuuuzym dodatkiem
> pewnego Greka:))

Sprzet zrobiony przez Polakow, ale oprogamowanie ktore tak chwalisz
od Brytyjczykow.

Na skale krajowa to bylo osiagniecie. Ale pod wzgledem technologiczym
jak Odry wchodzily do produkcji seryjnej to byly jakies 5-7 lat
do tylu w stusunku do zachodu. Urbanek pisze ze Odra to duza maszyna
i porownuje mozliwosci obliczeniowe Odry 1305 do IBM370/145. Tyle ze
145 to pogranicze maszyn malych i srednich. IBM mial znacznie wieksze
maszyny. Ruscy mieli BESM-6.

Co do oprogramowania, to bylo w zasadzie nierozwojwe. Tzn. podstawowe
adresy Odry to 15 bitow i to w 1973 bylo malo jak na mainframe.
Bylo rozszerzenie do 22 bitow, ale juz to wprowadzalo komplikacje.
24 bitowe rejestry oznaczaly ze wydluzenie adresu powyzej 24 bitow
wiazalo by sie z duzym problemem. IBM od 1965 mial adresy do 24
bitow. W czasie gdy produkcja Odry szla pelna para IBM wydluzal
adresy do 31 bitow, zas DEC wprowadzal 32 bitowego VAX-a zamiast
maszyn z krotszymi adresami.

Mysle ze najlepszym podsumowaniem jest tu koniec u Urbanka:
jak zniknely ogranicznia COCOM to Odra w Polsce stacila
wszelki sens ekonomiczny.

--
Waldek Hebisch
h...@m...uni.wroc.pl

do góry

W dniu 2015-09-10 21:16, Sebastian Biały pisze:

> Do Odry mam szacunek. Do ludzi gloryfikujących jej zastosowanie w PKP do
> XXI w nie mam ani grosza szacunku. To było głupie. Tak samo jak
> utrzymywanie Elixira i 90% gównianych systemów za grubą kasę zamawianych
> przez administrację publiczną za które jako programista się
> najzwyczajniej wstydzę.

Prawda jest taka, ze zależy do czego ją stosowano. Faktem jest, że jeśli
np do prostego sterowania, gdzie komunikacja na jakiś liniach odbywa się
jeszcze ciągle z prędkością 50 bodów (bo kable nie pozwalają na więcej),
to spokojnie powinno dać sobie radę i dopóki nie wyremontuje się linii,
to zmiana sprzętu może być nieopłacalna, skoro działa...



--
Kaczus
http://kaczus.ppa.pl/art/komputery-prl,27.html
http://kaczus.republika.pl

do góry