[21.01.2020 16:29:39] <bartosz> Przeczytaj o Klee.
[21.01.2020 16:29:55] <bartosz> Wiesz już, co to znaczy "model checking"?
[21.01.2020 16:30:02] <bartosz> Albo "full model construction"?
[21.01.2020 16:31:25] <juliusz.t@haael.com.pl> Model Checking?
[21.01.2020 16:31:38] <bartosz> Wiesz, co to oznacza?
[21.01.2020 16:31:59] <juliusz.t@haael.com.pl> Polega na stworzeniu wiernego modelu układu.
[21.01.2020 16:32:11] <bartosz> Polega na sprawdzeniu wszystkich wartości po kolei.
[21.01.2020 16:32:23] <juliusz.t@haael.com.pl> No, nie zawsze, ale tak.
[21.01.2020 16:32:44] <bartosz> Polega na udowodnieniu kwantyfikatora "dla każdego x" przez fizyczne wykonanie kodu dla każdego x.
[21.01.2020 16:32:48] <bartosz> To jest model checking.
[21.01.2020 16:33:02] <bartosz> Ma złożoność taką, jak rozmiar dziedziny.
[21.01.2020 16:33:11] <bartosz> Jest lepsza metoda.
[21.01.2020 16:33:15] <bartosz> Którą my użyjemy.
[21.01.2020 16:33:25] <bartosz> Jest ona wykorzystywana w klee.
[21.01.2020 16:33:32] <bartosz> Przeczytaj dokładnie, czym jest klee.
[21.01.2020 16:33:36] <bartosz> I naucz tego Maćka.
[21.01.2020 16:36:29] <juliusz.t@haael.com.pl> Okej.
[21.01.2020 16:37:01] <juliusz.t@haael.com.pl> (BTW Jabber dalej nie ma dobrych klientów. PSI kraszuje mi się na Windowsie i muszę restartować cały system.)
[21.01.2020 16:37:51] <bartosz> To raczej problem z Windowsem niż Psi a tym bardziej z Jabberem.
[21.01.2020 16:38:57] <juliusz.t@haael.com.pl> To problem Jabbera, że nie ma dobrych komunikatorów
[21.01.2020 16:39:16] <bartosz> Paulina robi tutorial?
[21.01.2020 16:39:26] <bartosz> Potrzebuję trzech rzeczy.
[21.01.2020 16:39:33] <juliusz.t@haael.com.pl> Tłumaczenie? Wczoraj coś robiła.
[21.01.2020 16:39:34] <bartosz> Pluginu, na podstawie tutoriala.
[21.01.2020 16:39:45] <bartosz> Biblioteki do wyświetlania SVG.
[21.01.2020 16:39:52] <bartosz> I samego interfejsu.
[21.01.2020 16:39:56] <bartosz> I mamy komunikator.
[21.01.2020 16:40:12] <juliusz.t@haael.com.pl> Który będzie się wywalał, ale to pewnie przez system. ;)
[21.01.2020 16:40:22] <juliusz.t@haael.com.pl> Albo będzie działać tylko na jednej platformie.
[21.01.2020 16:40:31] <juliusz.t@haael.com.pl> I nie będzie oferować historii rozmów. :P
[21.01.2020 16:40:33] <bartosz> Mamy odpowiednik apek webowych, które można uruchamiać gdziekolwiek.
[21.01.2020 16:40:41] <bartosz> Historii nie.
[21.01.2020 16:40:52] <bartosz> Czy historia jest zapamiętywana na serwerze?
[21.01.2020 16:41:05] <bartosz> To moje coś nie będzie tworzyć żadnych plików na komputerze.
[21.01.2020 16:41:09] <juliusz.t@haael.com.pl> U nas chyba nie.
[21.01.2020 16:41:16] <juliusz.t@haael.com.pl> Nie wiem, czy Ty tego nie wyłączyłeś.
[21.01.2020 16:41:23] <bartosz> Czy XMPP ma opcję zapisywania historii na serwerze?
[21.01.2020 16:41:34] <juliusz.t@haael.com.pl> Jako użytkownik nie chciałbym o tym wiedzieć. :P
[21.01.2020 16:41:42] <bartosz> Lol.
[21.01.2020 16:41:52] <bartosz> W każdym razie chcę klienta bezstanowego.
[21.01.2020 16:42:12] <bartosz> Logujesz się z dowolnego miejsca i zawsze robi to samo, bo nie ma niczego na dysku.
[21.01.2020 16:45:05] <juliusz.t@haael.com.pl> Szkoda, że bezstanowy nie implikuje, że będzie dobry.
[21.01.2020 16:52:36] <bartosz> Dla mnie dobry = minimalny.
[21.01.2020 16:52:44] <bartosz> Im coś ma mniej opcji, tym lepiej.
[21.01.2020 16:53:00] <bartosz> Lepiej mieć jedną opcję dopracowaną w 100%, niż 100 opcji każdą na 1%.
[21.01.2020 16:53:22] <bartosz> Więc będzie miał tylko obsługę tekstu, SVG i XForms.
[21.01.2020 16:53:31] <juliusz.t@haael.com.pl> Einstein kiedyś powiedział: "Powinno to być tak proste, jak to możliwe, ale nie prostsze."
[21.01.2020 16:53:32] <bartosz> Ale z tych trzech rzeczy można zbudować wszystko.
[21.01.2020 16:53:37] <bartosz> Tak.
[21.01.2020 16:53:57] <bartosz> XMPP zamiast HTTP.
[21.01.2020 16:54:00] <juliusz.t@haael.com.pl> Chamie, żeby się komunikować potrzebuję dobrego komunikatora.
[21.01.2020 16:54:02] <bartosz> SVG zamiast HTML.
[21.01.2020 16:54:18] <bartosz> XForms zamiast HTMLowych formularzy i Javascriptu.
[21.01.2020 16:54:23] <juliusz.t@haael.com.pl> Od komunikatora oczekuję, że będę mógł nadawać, obierać i składować wiadomości.
[21.01.2020 16:54:24] <bartosz> Tekst jako fallback.
[21.01.2020 16:54:43] <juliusz.t@haael.com.pl> Dodatkowo, ma być dostępny wszędzie.
[21.01.2020 16:54:49] <bartosz> To już zadanie dla twórcy interfejsu.
[21.01.2020 16:54:51] <juliusz.t@haael.com.pl> Na każdej platformie.
[21.01.2020 16:54:57] <bartosz> Ktoś będzie musiał zbudować interfejs.
[21.01.2020 16:55:02] <bartosz> Designer.
[21.01.2020 16:55:06] <juliusz.t@haael.com.pl> Ja jestem użytkownikiem.
[21.01.2020 16:55:19] <juliusz.t@haael.com.pl> Nie jestem developerem XMPP, tylko użytkownikiem na Boga.
[21.01.2020 16:55:42] <bartosz> Tylko Ci mówię, jaką drogę wybrałem.
[21.01.2020 16:55:46] <bartosz> I uważam, że jest dobra.
[21.01.2020 16:55:47] <juliusz.t@haael.com.pl> Jestem od Ciebie jeszcze warstwę dalej, niż designer.
[21.01.2020 16:56:06] <juliusz.t@haael.com.pl> Szkoda, że ta droga ma służyć do komunikacji, a podążasz nią sam.
[21.01.2020 16:56:07] <bartosz> Tzn. że przyciągnie designerów w takim samym sensie, jak HTML stworzył profesję webmasterów.
[21.01.2020 16:56:16] <juliusz.t@haael.com.pl> Zatraciłeś gdzieś cel w tej podróży. ;)
[21.01.2020 16:56:34] <juliusz.t@haael.com.pl> Właśnie się przyznałeś.
[21.01.2020 16:56:42] <juliusz.t@haael.com.pl> Nie używasz XMPP do komunikacji.
[21.01.2020 16:56:46] <juliusz.t@haael.com.pl> Masz inny cel.
[21.01.2020 16:57:17] <juliusz.t@haael.com.pl> Twój klient będzie realizował inne cele, niż zapewnienie komunikacji między ludzmi.
[21.01.2020 16:58:09] <juliusz.t@haael.com.pl> Więc proponuję Ci przerzucenie się na coś innego, np. Skype, Messengera lub cokolwiek, co faktycznie służy komunikacji i niczemu więcej. :P
[21.01.2020 16:58:37] <bartosz> :)
[21.01.2020 16:59:07] <bartosz> HTTP też służy do komunikacji a zbudowali na nim znacznie więcej.
[21.01.2020 17:00:41] <juliusz.t@haael.com.pl> "Powinno to być tak proste, jak to możliwe, ale nie prostsze."
[21.01.2020 17:01:00] <juliusz.t@haael.com.pl> HTTP nie służy do komunikacji.
[21.01.2020 17:01:00] <bartosz> :)
[21.01.2020 17:01:08] <juliusz.t@haael.com.pl> Służy do transferu plików.
[21.01.2020 17:01:58] <bartosz> Do transferu plików służy BitTorrent.
[21.01.2020 17:02:37] <juliusz.t@haael.com.pl> HTTP (ang. Hypertext Transfer Protocol) – protokół przesyłania dokumentów hipertekstowych.
[21.01.2020 17:02:44] <juliusz.t@haael.com.pl> Przesyła dokumenty.
[21.01.2020 17:02:54] <juliusz.t@haael.com.pl> Przesyłanie to nie jest komunikacja.
[21.01.2020 17:03:30] <bartosz> A WebRTC?
[21.01.2020 17:04:20] <juliusz.t@haael.com.pl> WebRTC (Web Real-Time Communication) is a free, open-source project that provides web browsers and mobile applications with real-time communication (RTC) via simple application programming interfaces (APIs). It allows audio and video communication to work inside web pages by allowing direct peer-to-peer communication, eliminating the need to install plugins or download native apps.
[21.01.2020 17:05:05] <bartosz> To jest komunikacja za pomocą HTTP między klientami.
[21.01.2020 17:05:39] <juliusz.t@haael.com.pl> Komunikacja to proces nadawania i odbierania wiadomości.
[21.01.2020 17:05:47] <juliusz.t@haael.com.pl> Od komunikatora oczekuje, że mi z tym pomoże.
[21.01.2020 17:05:55] <juliusz.t@haael.com.pl> Jabber nie ma dobrych komunikatorów.
[21.01.2020 17:06:10] <bartosz> Nie ma dobrych interfejsów.
[21.01.2020 17:06:17] <bartosz> Ktoś musi stworzyć interfejs.
[21.01.2020 17:06:26] <juliusz.t@haael.com.pl> A raczej - są inne klienty, które zapewniają komunikację na wyższym poziomie.
[21.01.2020 17:06:34] <juliusz.t@haael.com.pl> Nie interesuje mnie co mają w środku.
[21.01.2020 17:06:41] <juliusz.t@haael.com.pl> Jestem użytkownikiem, a nie developerem.
[21.01.2020 17:06:57] <juliusz.t@haael.com.pl> Nie chcę sobie stworzyć interfejsu, tylko dostać gotowy produkt.
[21.01.2020 17:08:56] <bartosz> Co raz zobaczyłeś, tego nie da się już odzobaczyć.
[21.01.2020 17:09:06] <bartosz> Już nigdy nie zapomnisz, jak działa Jabber :).
[21.01.2020 18:27:26] <juliusz.t@haael.com.pl> Mam problem z zarządzaniem wiadomościami na liście mailowej.
[21.01.2020 18:27:39] <juliusz.t@haael.com.pl> Które wiadomości na pewno nie są istotne?
[21.01.2020 18:28:00] <juliusz.t@haael.com.pl> Dostaję zgłoszenia o bugach. Czy może się pojawić tam coś, co dotyczy stricte nas?
[21.01.2020 19:34:27] <bartosz> Nie.
[21.01.2020 19:34:36] <bartosz> Tylko my coś takiego wysyłamy :).
[21.01.2020 19:34:40] <bartosz> My robimy dowody.
[21.01.2020 19:34:46] <bartosz> Tamto to są developerzy.
[21.01.2020 19:41:42] <juliusz.t@haael.com.pl> Okej.
[21.01.2020 19:41:57] <juliusz.t@haael.com.pl> Prosili, żebyśmy się przedstawili, ale jeszcze tego nie zrobiłem.
[21.01.2020 19:42:03] <juliusz.t@haael.com.pl> Kiedyś coś tam napiszę.
[21.01.2020 19:42:04] <bartosz> Naucz Maćka o tym podejściu klee.
[21.01.2020 19:42:12] <juliusz.t@haael.com.pl> Właśnie czytam o tym.
[21.01.2020 19:42:17] <juliusz.t@haael.com.pl> Ale używają trudnych słów.
[21.01.2020 19:42:40] <bartosz> Nie obiecywałem, że będzie łatwo to wymówić.
[22.01.2020 11:49:07] <juliusz.t@haael.com.pl> Istnieje już kilkanaście implementacji RISC-V.
[22.01.2020 11:49:12] <juliusz.t@haael.com.pl> Po co robić następną?
[22.01.2020 11:49:21] <bartosz> Bo jest nasza?
[22.01.2020 11:49:28] <bartosz> Poza tym tamte nie mają dowodu, tak?
[22.01.2020 11:49:37] <bartosz> Rozumiesz już działanie klee?
[22.01.2020 11:49:42] <juliusz.t@haael.com.pl> Uczę się właśnie.
[22.01.2020 11:49:47] <juliusz.t@haael.com.pl> Ale generalnie widzę o co chodzi.
[22.01.2020 11:49:55] <bartosz> Wyjaśnij.
[22.01.2020 11:50:06] <juliusz.t@haael.com.pl> Tłumaczy kod do LLVM.
[22.01.2020 11:50:27] <juliusz.t@haael.com.pl> Następnie nie podstawia konkretnych wartości, tylko zmienne, do których przypisane są własności.
[22.01.2020 11:51:35] <juliusz.t@haael.com.pl> I jeśli jest wykonywana operacja, to sprawdza, czy nie jest ona niebezpieczna na ogólnym zbiorze, a nie na wartości (np. czy któraś wartość ze zbioru nie wychodzi poza zakres pamięci).
[22.01.2020 11:51:47] <bartosz> Jaki widzisz związek z tym, co robimy w Pythonie?
[22.01.2020 11:52:06] <bartosz> (A do zmiennych w klee nie są przypisane wartości.)
[22.01.2020 11:52:08] <juliusz.t@haael.com.pl> Możemy zamiast LLVM analizować samego Pythona?
[22.01.2020 11:52:28] <bartosz> Napisałeś moduł do arytmetyki modulo.
[22.01.2020 11:52:38] <bartosz> Oraz klasę tworzącą wyrażenia.
[22.01.2020 11:52:48] <bartosz> Jaki widzisz związek z klee?
[22.01.2020 11:53:15] <bartosz> Gdyby stworzyć dwie zmienne w tej klasie od wyrażeń.
[22.01.2020 11:53:27] <bartosz> Tzn. dwa obiekty będące zmiennymi symbolicznymi.
[22.01.2020 11:53:51] <bartosz> Następnie stworzyć dwa obiekty modulo, gdzie zamiast wartości int dajemy im te zmienne symboliczne.
[22.01.2020 11:53:57] <bartosz> A następnie dodać je do siebie.
[22.01.2020 11:54:03] <bartosz> Tzn. te modulo.
[22.01.2020 11:54:06] <bartosz> Co by powstało?
[22.01.2020 11:54:12] <juliusz.t@haael.com.pl> Będziemy mieli wyrażenie, a nie wartość.
[22.01.2020 11:54:59] <bartosz> Jaki widzisz związek z klee?
[22.01.2020 11:55:46] <juliusz.t@haael.com.pl> Klee też korzysta z wartości.
[22.01.2020 11:55:53] <juliusz.t@haael.com.pl> *z wyrażeń.
[22.01.2020 11:55:56] <bartosz> Ech.
[22.01.2020 11:56:02] <bartosz> No tak. Ale jak działa klee?
[22.01.2020 11:56:12] <bartosz> Co robi klee i co robi nasz system?
[22.01.2020 11:56:14] <bartosz> Jaka jest idea?
[22.01.2020 11:56:29] <bartosz> W ogóle rozumiesz, jaki to ma związek z dowodzeniem?
[22.01.2020 11:57:28] <juliusz.t@haael.com.pl> Nie będę zgadywać. Rozumiem, ale nie wiem jakiej odpowiedzi ode mnie oczekujesz.
[22.01.2020 11:58:02] <juliusz.t@haael.com.pl> Samo to, że mamy wyrażenia pozwala formułować własności działań, jakie wykonujemy.
[22.01.2020 11:58:30] <juliusz.t@haael.com.pl> Dowiedzenie posiadania własności jest równoważne, ze spełnieniem jakichś aksjomatów.
[22.01.2020 11:58:36] <bartosz> Uzasadnij, że klee albo nasz system jest w stanie udowodnić, że dana formuła z funkcją w LLVM / Pythonie jest spełniona dla wszystkich wartości.
[22.01.2020 11:58:52] <bartosz>
def f(x):
 return cośtam

[22.01.2020 11:59:12] <bartosz> FORALL(x) valid( f( x ) )
[22.01.2020 11:59:15] <bartosz> Ech.
[22.01.2020 11:59:24] <bartosz> FORALL( x ) valid( f( x ) )
[22.01.2020 11:59:39] <bartosz> Masz jakąś funkcję f, w Pythonie.
[22.01.2020 11:59:43] <bartosz> Analogicznie: w LLVM.
[22.01.2020 12:00:14] <bartosz> Ta funkcja nie ma skutków ubocznych ani pętli nie-stałej wielkości (czyli jest obwodem), poza tym może być dowolna.
[22.01.2020 12:00:39] <bartosz> W szczególności może zawierać konstrukcje imperatywne, może się też odwoływać do innych funkcji spełniających te same warunki.
[22.01.2020 12:00:44] <bartosz> Nie ma rekurencji.
[22.01.2020 12:00:58] <bartosz> Uzasadnij, że nasz system albo klee udowodni tą formułę.
[22.01.2020 12:01:31] <bartosz> valid może być też dowolnym predykatem.
[22.01.2020 12:02:00] <bartosz> Wygląda na to, że nie rozumiesz tego jeszcze do końca.
[22.01.2020 12:02:08] <juliusz.t@haael.com.pl> W poradniku inżyniera była reguła wnioskowania "opuszczenia kwantyfikatora ogólnego".
[22.01.2020 12:02:09] <bartosz> Dokończ ten Twój moduł od wyrażeń.
[22.01.2020 12:02:25] <bartosz> Nie w poradniku inżyniera. Jak działa klee?
[22.01.2020 12:02:32] <bartosz> Dokończ ten moduł od wyrażeń.
[22.01.2020 12:02:47] <bartosz> Stwórz dwie zmienne (reprezentujące pythonowe inty).
[22.01.2020 12:03:03] <bartosz> Stwórz dwa obiekty modulo z tymi zmiennymi w miejsce wartości.
[22.01.2020 12:03:25] <bartosz> x = Expression.var('x')
[22.01.2020 12:03:31] <bartosz> y = Expression.var('y')
[22.01.2020 12:03:37] <bartosz> a = Modulo(x)
[22.01.2020 12:03:40] <bartosz> Ech.
[22.01.2020 12:03:43] <bartosz> a = Modulo( x )
[22.01.2020 12:03:47] <bartosz> b = Modulo( y )
[22.01.2020 12:03:52] <bartosz> Udowodnij:
[22.01.2020 12:04:49] <bartosz> FORALL( x, y ) a + b = b + a
[22.01.2020 12:05:10] <bartosz> FORALL( x, y, z ) (a + b) + c == a + (b + c)
[22.01.2020 12:05:23] <bartosz> FORALL( x ) a + Modulo( 0 ) == a
[22.01.2020 12:05:35] <bartosz> FORALL( x ) a + Modulo( 1 ) != a
[22.01.2020 12:05:47] <bartosz> Aksjomaty arytmetyki modulo.
[22.01.2020 12:05:54] <bartosz> Jest jeszcze jeden aksjomat, ale jest długi.
[22.01.2020 12:06:04] <bartosz> Na razie wystarczy, że udowodnisz jeden, dowolny.
[22.01.2020 12:06:24] <bartosz> A w zasadzie: wytłumacz, w jaki sposób klee / nasz system to udowadnia i dlaczego w ogóle to jest dobry dowód.
[22.01.2020 12:07:15] <bartosz> Czy zgadzasz się, że gdyby w jakiś sposób fizycznie sprawdzić te aksjomaty dla wszystkich kombinacji intów po kolei, to to byłby dobry dowód?
[22.01.2020 12:08:08] <juliusz.t@haael.com.pl> Sprawdzenie wszystkich elementów w teorii skończonej to to samo co sprawdzenie formuły z kwantyfikatorem ogólnym.
[22.01.2020 12:08:20] <bartosz> Nieskończonej też :).
[22.01.2020 12:08:27] <bartosz> Na komputerze się nie da, ale matematycznie można.
[22.01.2020 12:08:44] <bartosz> Teraz pokaż, że klee też udowadnia kwantyfikator ogólny.
[22.01.2020 12:08:57] <bartosz> Ale bez sprawdzania wszystkich wartości.
[22.01.2020 12:09:02] <bartosz> Zazwyczaj.
[22.01.2020 12:09:10] <bartosz> Co innego jest złożonością klee.
[22.01.2020 12:09:33] <bartosz> Klee jest ograniczone innym parametrem, nie rozmiarem dziedziny. Jakim?
[22.01.2020 12:09:42] <bartosz> Co decyduje o czasie działania klee?
[22.01.2020 12:11:01] <juliusz.t@haael.com.pl> Chamie, zle się z Tobą pracuje. Jesteś strasznie agresywny w wpowiedziach.
[22.01.2020 12:11:09] <juliusz.t@haael.com.pl> Doczytam o klee i wtedy wrócę.
[22.01.2020 12:11:13] <bartosz> OK.
[22.01.2020 12:11:19] <juliusz.t@haael.com.pl> Postaram się zrobić to zadanie z modulo.
[22.01.2020 12:11:23] <bartosz> OK.
[22.01.2020 12:13:19] <juliusz.t@haael.com.pl> Moja odpowiedz jest taka, że do dowodu z ogólnym wyrażeniem można wprowadzić kwantyfikator ogólny, tak jak w regułach opuszczenia i wprowadzania kwantyfikatora ogólnego.
[22.01.2020 12:13:30] <juliusz.t@haael.com.pl> Jak będę miał lepszą, to napiszę.
[22.01.2020 12:14:01] <bartosz> Przeczytaj, co robi klee, kiedy napotka ifa.
[22.01.2020 12:14:04] <bartosz> Warunek.
[22.01.2020 12:14:13] <bartosz> Twój moduł też.