Menu główne
Spotkania robocze zespołu projektu Lingua w roku 2026
- Utworzono: sobota, 17 maj 2025 15:13
- Poprawiono: sobota, 09 maj 2026 15:20
- Odsłony: 363
Poza spotkaniami zespołu, na których przedstawiam podstawy teoretyczne wprowadzające do projektu Lingua, spotykamy się również w celu prowadzenia rozmów o przyszłości projektu i jego stanie aktualnym. Niniejsza strona służy do dokumentowania i archiwizowania tych rozmów.
2026 01 03 Spotkanie na temat ekosystemów dla programistów w Lingua
Spotkanie było niezwykle bogate w debatę, choć praktycznie nie na temat ekosystemów. Powróciliśmy natomiast do "korzeni", a więc do zasad projektowania języków od denotacji do składni. Dla mnie było to bardzo ciekawe doświadczenie. Umówiliśmy się na następne spotkanie za tydzień, tj. w sobotę 10 stycznia o godz. 13:00. Jako materiał ze spotkania zamieszczam jedynie wideo, bo żadnej prezentacji, ani raportu nie pokazywałem. Posługiwałem się jedynie książką. Tej jednak nie zamieszczam, bo nad rozdziałami o ekosystemach jeszcze pracuję. Może za jakiś tydzień będę gotów, to wtedy udostępnię. W naszej debacie odwoływaliśmy się do rozdziałów, które już od dawna są w książce dostępnej na witrynie.
2026 01 03 Spotkanie na temat ekosystemów dla programistów w Lingua c.d.
Tym razem pokazałem dużo nowych szczegółów dotyczących projektu ekosystemu. Pokazałem je też w nieco innej wersji niż na poprzednich spotkaniach. Wydaje mi się, że obecnie lepiej rozumiem, czym takie ekosystemy powinny być. Załączam nagranie i prezentację. Następne spotkanie wyznaczyliśmy na sobotę 24 stycznia 2026 godz. 13:00 - 15:00. Opowiem na nim o tym, co uda mi się zrobić przez najbliższe dwa tygodnie, bo tym razem mojej historii o ekosystemach nie dokończyłem. I prawdę mówiąc, długo jeszcze pewnie nie zakończę.
Pobierz prezentację z 2026 01 11
2026 01 24 Spotkanie na temat ekosystemów dla programistów w Lingua c.d.
Na tym spotkaniu podsumowałem (uporządkowany w międzyczasie) materiał dotyczący ekosystemu, kończąc pewien wstępny etap pracy nad tym tematem. Kilka dni później zakończyłem też pracę nad dwoma rozdziałami książki poświęconymi ekosystemom. To z kolei spowodowało, że wprowadziłem kilka niewielkich zmian technicznych w prezentacji. Ta, którą udostępniam poniżej, nie jest więc do końca spójna z prezentacją używaną podczas wykładu, ale za to jest zgodna z książką, której nowa wersja z dnia 29 stycznia 2026 r. jest już dostępna do pobrania. Najbliższe spotkanie zaplanowaliśmy na sobotę 14 lutego godz. 13:00.
Pobierz prezentację z 2026 01 29
2026 02 14 Spotkanie poświęcone przykładowi budowania programu
Program, którego budowanie/wyprowadzanie pokazałem, został mi zasugerowany przez Tomka Gieorgijewskiego z naszej ochotniczej grupy, za co serdecznie mu w tym miejscu dziękuję. W największym skrócie można powiedzieć, że dotyczy on mechanizmu kasy pancernej z szyfrowym zamkiem obsługiwanym przez pokrętło. Wydaje mi się, że to ciekawy przykład, bo pokazuje, jak zacząć pracę nad przyszłym programem od zbudowania matematycznego modelu mechanizmu, który ma być obsługiwany przez program. W moim wystąpieniu posługiwałem się nie prezentacją w PowerPoincie, ale maszynopisem artykułu, który właśnie piszę. Nie udostępniam jednak artykułu w wersji z 14 lutego, ale dzisiejszą jego wersję, poważnie rozbudowaną w stosunku do poprzedniej.
W trakcie pracy nad tym artykułem okazało się, że trzeba poszerzyć dotychczasowy model naszego ekosystemu w taki sposób, aby było możliwe jego rozbudowanie — a wraz z nim leżącej u jego podstaw teorii — o nowe symbole funkcyjne, a może też o nowe kategorie składniowe. Opisałem więc skrótowo, jak widzę możliwość takiego wzbogacania ekosystemu, w jednostronicowym tekście, który załączam wraz z artykułem podstawowym. Byłbym bardzo zainteresowany Waszymi uwagami na oba tematy.
Pobierz artykuł o budowania programu
Pobierz artykuł o wzbogacaniu ekosystemów
2026 02 21 Spotkanie poświęcone rozbudowanemu przykładowi budowania programu
Zaproponowałem pewną systematykę w budowaniu programu w trzech krokach:
- budowanie modelu matematycznego opisujące zjawisko lub mechanizm, którego ma dotyczyć program,
- budowanie teorii sformalizowanej dla tego modelu, tj. lematów, które zostają zapisane w repozytorium,
- budowanie kodu programu na podstawie zawartości repozytorium.
Rozbudowałem też program o pętlę while, która wykonuje kolejne rotację z ich ciągu zadanego na wejściu programu. Jak zwykle po prezentacji, wysłuchaniu uwag słuchaczy, a także samego siebie, doszedłem do wniosku, że parę rzeczy trzeba uściślić. I to właśnie zrobiłem w nowej wersji pracy gotowej do pobrania poniżej.
Pobierz artykuł o budowaniu programu z 2026 02 27
2026 02 28 Kolejne spotkanie poświęcone przykładowi budowania tego samego programu
Na znanym nam już przykładzie pokazałem pewne problemy teoretyczne i praktyczne, które wymagają naszej uwagi, gdy budujemy teorię sformalizowaną w języku Lingua-T, dla rozszerzonego modelu Lingua-V. Rozmawialiśmy też o adekwatności specyfikacji programu, który chcemy budować.
Niezależnie od naszego przykładu, choć nim inspirowane, omówiłem wprowadzenie do Lingua-V dwóch nowych pojęć: stałej (obok zmiennej) i stałej fantomowej. Pokazałem posługując się właśnie modyfikowanym tekstem książki (jeszcze nie ma jej na stronie), jak zmieniają się w związku z tymi pojęciami definicje trzech konstruktorów:
- konstruktora denotacji wyrażeń wartościologicznych (value expressions),
- konstruktora denotacji instrukcji przypisania,
- funkcji opisującej przekazywanie parametrów aktualnych do wywołania procedury.
2026 03 07 Pierwsze spotkanie poświęcone budowaniu dziedzinowego języka specyfikacji do zastosowań w projektowaniu pojazdów autonomicznych
Rozważamy przykład budowania języka kontraktu (specyfikacji) do dialogu pomiędzy inżynierem budującym pojazdy samobieżne a informatykiem piszącym oprogramowanie dla takich pojazdów. Przykład jest oparty na realiach związanych z przemysłem samochodowym. Wspólnie z Pawłem Paterkiem, informatykiem z doświadczeniem w tym obszarze, staramy się zaprojektować taki język specyfikacji. Na spotkaniu pokazaliśmy przykład specyfikacji napisanej w notacji, którą traktujemy jako prototyp przyszłego języka. Na tym etapie udostępniam jedynie nagranie, gdyż nasz raport jest w bardzo wczesnej fazie pisania, co powoduje, że co chwila pojawiają się nowe wersja różniące się od poprzednich.
2026 03 14 Drugie spotkanie poświęcone budowaniu rozszerzenia j. Lingua do zastosowań w projektowaniu pojazdów autonomicznych
Rozważaliśmy ten sam przykład, co poprzednio, ale w nieco innej formalizacji. M.in. wprowadziłem klasy, by mieć zmienne prywatne i pokazałem przemysłowy przykład specyfikacji wymagań dla pojazdu. Zastanawiam się nad użyciem do specyfikacji sieci Petriego. Może uda mi się coś przygotować na następne spotkanie. Umówiliśmy się za dwa tygodnie, w sobotę 14 marca o godz. 11:00. Tekstu raportu nie umieszczam na stronie, bo to nadal bardzo nieuczesana wersja. Nasz przyszły język nazwaliśmy roboczo Lingua-AV (AV - autonomous vehicles)
2026 03 28 Trzecie spotkanie poświęcone Lingua-VA - strategie jako sieci Petriego
Pokazuję rozwiązanie dalece różne od poprzedniego, bo strategie są opisane sieciami Petriego. To bardzo wstępna wersja, więc ponownie nie załączam prezentacji.
2026 05 09 Środowisko programisty dla Lingua-V
Marek Jaźwiński przedstawił własną koncepcję takiego środowiska. Będziemy poszukiwać osób zainteresowanych pracami realizacyjnymi przy jego budowaniu.
Presentations to the course at Warsaw University in the spring semester 2020/21
- Utworzono: poniedziałek, 24 luty 2020 06:44
- Poprawiono: poniedziałek, 07 czerwiec 2021 13:32
- Odsłony: 14749
This section provides access to the presentations for the course “Denotational Engineering of Programming Languages” conducted during the spring semester of the academic year 2020/2021 at the Department of Mathematics, Informatics, and Mechanics of Warsaw University.
Presentations will be updated as comments are received from listeners. The names of updated files will not change, but the date of the last modification will be shown on this site. To download a file, click on its name. Section numbers seen in front pages of presentations refer to the book “A Denotational Engineering of Programming Languages,” which can also be downloaded from this page.
0 A.Blikle - An invitation to a project.pdf by March 1st, 2021
The description of what the project is about.
0 A.Blikle - Jak to zrobimy.pdf (How we shall we do it) by March 1st, 2021
This presentation is exceptionally in Polish. It explains the idea of how our project will be realized by the group of listeners of the course organized as an innovative startup, which should be a self-organizing team (a teal teem). More on teal organizations in the book of Andrzej Blikle "A Teal Doctrine of Quality" (or in Polish “Turkusowa doktryna Jakości”), both to be downloaded from this site.
1 A.Blikle - DEPL Preliminaries.pdf by March 8th, 2021
Preliminary concepts and notations: Chain-complete partially ordered sets (CPOs), CPO of formal languages and equational grammars, many-sorted algebras, CPO od binary relations, and of domains, abstract errors, a three-valued propositional calculus. Sections 2.1 - 2.9
2 A.Blikle - DEPL Many-sorted algebras.pdf by March 8th, 2021
Many-sorted algebras in general. Algebras of syntax. Abstract, concrete and colloquial syntax. Ambiguous and unambiguous algebras. Algebras of syntax versus equational grammars. Sections 2.20 - 2.14
3 A.Blikle - DEPL Lingua-A From data to values.pdf by March 15th, 2021
Data, bodies, composites, yokes, and values. The fundament for Lingua-A that constitutes an applicative layer of Lingua. Sections 4.1 - 4.3.
4 A.Blikle - DEPL Lingua-A Expressions.pdf by March 18th, 2021
Data expressions, and type-expressions. Sections 4.4. - 4.8
5 A.Blikle - DEPL Lingua-1 Instructions and declarations.pdf by March 23rd, 2021
Declarations, instructions (without procedures), and programs. Section 5.
6 A.Blikle - DEPL Lingua-2 Procedures.pdf by March 25th, 2021
Imperative procedures with recursion and multirecursion, and functional procedures. Section 6.
7 A.Blikle - DEPL Semantic correctness of programs.pdf by May 21st, 2021
An introduction to program correctness + partial correctness. Sections 7.1 - 7.6
8 A.Blikle - DEPL Total correctness of programs.pdf by May 21st, 2021
Weak total correctness in the relational framework. Section 7.7
9 A.Blikle - DEPL Lingua-2V Syntax and semantics.pdf by May 27th, 2021
Weak total correctness in the relational framework. Sections 8.1 - 8.4
10 A.Blikle - DEPL Lingua-2V Program-construction rules.pdf by May 31st, 2021
Rules for the development of correct programs in Lingua-2V. Section 8.5
11 A.Blikle - DEPL Lingua-2V Transformational programming.pdf by June 7th, 2021
Rules for the transformation of correct programs in Lingua-2V. Section 8.6
12 A.Blikle - DEPL Lingua-OO Object-oriented programming.pdf by April 27th, 2020
The expansion of the Lingua model to OO-programming. Section 8.6
Zaproszenie do projektu
- Utworzono: wtorek, 30 kwiecień 2019 11:26
- Poprawiono: sobota, 17 maj 2025 18:00
- Odsłony: 9182
Osobom zainteresowany rozwijaniem projektu, mogę zaoferować pomoc merytoryczną w tym obszarze, a także — być może — jakąś pomoc organizacyjną. Mogę się podjąć funkcji promotora prac magisterskich i doktorskich oraz przeprowadzenia kursów na różnych poziomach matematycznej szczegółowości w zależności od tego, czy słuchaczami byliby teoretycy zamierzający dalej rozwijać denotacyjny model Lingua, czy też praktycy zainteresowani budowaniem narzędzi wspomagających pracę projektanta języka lub programisty (patrz: Co jest jeszcze do zrobienia)
W dalszej perspektywie można by też myśleć o powołaniu start-up'u, który oferowałby wdrożenia narzędzi środowiska projektanta języków oraz programistycznego w technologii Lingua oraz opiekę na tymi narzędziami. Analogicznie jak w przypadkach implementacji Linuxa, same narzędzia pozostawałyby bezpłatne, natomiast komercjalizacji podlegałoby wsparcie w ich stosowaniu i aktualizowaniu. Firma mogłaby też oferować produkty IT zbudowane zgodnie z metodologią oferowaną przez środowisko programistyczne dla Lingua.
Osoby zainteresowane porozmawianiem o szczegółach projektu bardzo proszę o kontakt ze mną na adres Ten adres pocztowy jest chroniony przed spamowaniem. Aby go zobaczyć, konieczne jest włączenie w przeglądarce obsługi JavaScript. Polecam też zajrzenie na stronę Wykłady wprowadzające do projektu Lingua, gdzie można znaleźć nagrania i prezentacje z wykładów prowadzonych aktualnie dla grupy zainteresowanych osób.
Co już zrobiono
- Utworzono: środa, 01 maj 2019 14:32
- Poprawiono: środa, 01 maj 2019 14:32
- Odsłony: 6689
Ta sekcja obejmuje preprinty opublikowane w sieci na niniejszej witrynie a także na portalu ResearchGate. Główny materiał w projekcie, który stanowi książka, jest dostępny zarówno w wersji polskiej, jak i angielskiej. Pozostałe prace jedynie w języku angielskim. Wszelkie uwagi, rady i komentarze będą bardzo mile widziane. Proszę je kierować na adres Ten adres pocztowy jest chroniony przed spamowaniem. Aby go zobaczyć, konieczne jest włączenie w przeglądarce obsługi JavaScript.
Propozycja wykładu seminaryjnego
- Utworzono: wtorek, 30 kwiecień 2019 11:20
- Poprawiono: środa, 01 maj 2019 15:49
- Odsłony: 5854
Eksperyment z semantyką denotacyjną (odwracając tradycyjną kolej rzeczy) Pobierz prezentację
Wykład w wymiarze minimalnym (60 min) obejmuje strony od 1 do 15 prezentacji. Na pełen wykład trzeba przeznaczyć co najmniej 120 min plus odpowiednią ilość czasu na dyskusję.
Zapowiedź:
Czy można sobie wyobrazić, by klient kupujący samochód podpisywał zrzeczenie się wszelkich praw do roszczeń (ang. disclosure), gdyby wady techniczne samochodu miały narazić go na szkody? Chyba nie. To dlaczego w przemyśle IT jest to powszechny standard?
Moim zdaniem ten paradoks bierze się stąd, że podczas gdy każdy produkt techniczny powstaje na gruncie matematycznych obliczeń stanowiących swoisty „dowód jego poprawności”, to w informatyce takich dowodów — przynajmniej na skalę praktyczną — przeprowadzać nie umiemy.
Problem pozyskiwania matematycznych gwarancji poprawności programów pojawił się po raz pierwszy w pracy Alana Turinga w roku 1949. Później przez kilka dekad podejmowano ten temat badania pod hasłem dowodzenia poprawności programów, a równolegle też próby definiowania takich semantyk języków programowania, które byłyby podstawą do prowadzenia dowodów poprawności. Jednocześnie, od lat 1970. dla większości matematyków było raczej oczywiste, że matematyczne semantyki powinny być kompozycyjne, co oznacza, że znaczenie całości jest funkcją znaczeń jej części. W literaturze takie semantyki nazwano denotacyjnymi.
Niestety w żadnym z obu obszarów — semantyki i poprawność — nie dopracowano się metod, które weszłyby na stałe do repertuaru narzędzi inżynierii oprogramowania. Wreszcie zaniechano tych badań, co autorzy monografii Deductive Software Verification z roku 2016 podsumowali stwierdzając (tłumaczenie moje):
Przez wiele lat pojęcie formalnej weryfikacji było niemalże synonimem weryfikacji funkcjonalnej. W ostatnich latach staje się coraz bardziej jasne, że pełna funkcjonalna weryfikacja programu jest dla prawie wszystkich zastosowań celem iluzorycznym.
W mojej ocenie niepowodzenie opisanych wyżej prób miało dwa źródła:
Po pierwsze, dla większości istniejących języków programowania zapewne nie da się zbudować takiej semantyki, która mogłaby służyć do praktycznego dowodzenia poprawności programów. To oczywiście tylko opinia, ale fakt, że do tej pory nie udało się tego dokonać, o czymś jednak świadczy.
Po drugie, nawet gdyby taką semantykę zbudowano, to dla większości programów dowodów poprawności nie da się przeprowadzić z prostego powodu, że one poprawne nie są! Stąd też praktyczną wartość dowodzenia poprawności upatrywano w nadziei, że próba dowodzenia poprawności programu wskaże na zawarte w nim błędy.
W trakcie seminarium przedstawiam własną propozycję podjęcia problemów budowania semantyki denotacyjnej oraz poprawności programów, a także wyjaśniam, dlaczego wymaga ona „odwrócenia tradycyjnej kolei rzeczy”. Choć moja propozycja jest oparta na dość specyficznej matematyce, postaram się przedstawić ją w sposób strawny dla osób, które tej matematyki mogą nie znać. A tym, którzy chcieliby do niej sięgnąć, proponuję książkę (patrz: Książka).
Istnieją również wersje angielskie zarówno książki (The book), jak i wykładu (A proposal of a seminar). .
Za wszelkie opinie o metodzie, książce i wykładzie będę niezmiernie wdzięczny. Można do mnie pisać na adres Ten adres pocztowy jest chroniony przed spamowaniem. Aby go zobaczyć, konieczne jest włączenie w przeglądarce obsługi JavaScript..
