Menu główne
Spotkania robocze zespołu projektu Lingua
- Utworzono: sobota, 17 maj 2025 15:13
- Poprawiono: sobota, 13 wrzesień 2025 13:41
- Odsłony: 493
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.
2025 05 17 Pierwsze spotkanie po zakończeniu wstępnej serii wykładów
Na tym spotkaniu uczestnicy przedstawili się wzajemnie i wstępnie deklarowali obszar swoich zainteresowań w przyszłych pracach nad rozwojem projektu.
Pobierz streszczenie spotkania wykonane przez SI Zoom
2025 05 24 Spotkanie robocze
Na spotkaniu wystąpili:
- Roman Matuszewski, który mówił o swoich wstępnych refleksjach i zamierzeniach związanych z systemem automatycznego dowodzenia twierdzeń, który chcemy zainstalować w naszym ekosystemie programisty; to wystąpienie będzie kontynuowana na najbliższym spotkaniu,
- Marek Jaźwiński, który również mówił o swoich zamierzeniach, jednak dotyczących samego procesu budowania programów w Lingua; To wystąpienie będzie kontynuowane w czerwcu.
Pobierz streszczenie spotkania wykonane przez SI Zoom
2025 05 31 Spotkanie robocze
Na spotkaniu wystąpili:
- Roman Matuszewski, który mówił o swoich wstępnych refleksjach związanych z systemem automatycznego dowodzenia twierdzeń i w związku z tym zadawał wiele pytań Jackowi,
- Jacek Blikle, który na gruncie właśnie pisanej pracy omawiał swoje wstępne pomysły związane z formalizacją teorii denotacji, która byłaby podstawą działania w przyszłości systemu automatycznego dowodzenia twierdzeń wspomagającego pracę programisty w języku Lingua-V.
Pobierz streszczenie spotkania wykonane przez SI Zoom
2025 07 12 Spotkanie robocze
Spotkanie było poświęcone rozwinięciu myśli — omawianych na poprzednim spotkaniu — a poświęconych budowie sformalizowanej teorii, która stanowiłaby zaplecze dla ekosystemu programisty w językach typu Lingua-V, a w szczególności dla systemu automatycznego dowodzenia twierdzeń. Szczegółowo omówiono prosty przykład budowania programu poprawnego w takim środowisku, a także podstawową wiedzę dotyczącą sformalizowanych teorii pierwszego i drugiego rzędu. Wykład będzie kontynuowany za tydzień, tj. 2025 07 19.
2025 07 19 Spotkanie robocze
Spotkanie było poświęcone kontynuacji poprzedniego.Omówiłem proces (algorytm) budowania języka teorii sformalizowanej II rzędu dla języka z modelem algebraicznym. Następne spotkanie odbędzie się w sobotę 9 sierpnia
2025 08 09 Spotkanie robocze
Nadal opowiadałem o budowaniu języka teorii sformalizowanej, w którym można by mówić o własnościach denotacji języka Lingua-V. Poświęciłem też trochę czasu na omówienie mojej wizji logistyki pracy programisty w ekosystemie. W sumie omówiłem sporo materiału nieco ponad 2 godziny.
2025 08 23 Spotkanie robocze
Zdawało mi się, że będzie to ostatni wykład o budowaniu ekosystemów programisty, ale -- jak już nieraz -- okazało się, że jeszcze to i owo trzeba dodać. Trochę powtórzyłem i podsumowałem poprzednie wykłady o ekosystemie, ale też dodałem sporo nowego materiału. Wydaje mi się, że coraz lepiej rozumiem, o co w tym wszystkim chodzi.
2025 08 30 Spotkanie robocze
To było spotkanie kończące pierwszy cykl spotkań poświęconych zagadnieniom logicznym związanych z ekosystemem dla programistów w Lingua-V. Chyba już wiemy, jak powinien wyglądać przyszły ekosystem programisty, a przynajmniej wiemy od czego rozpocząć jego budowę. Do tego spotkania nie dołączam prezentację, bo jej pełną wersję udostępniam nieco niżej wraz z raportem podsumowującym moje wcześniejsze referaty.
Podsumowanie spotkań poświęconych logicznym aspektom ekosystemów dla programistów w Lingua-V (2025 09 13)
Pod tym nagłówkiem zamieszczam aktualną tekstową wersję moich wykładów. Jest to nadal wersja robocza, ale rozwinięta i zmodyfikowana w stosunku do poprzednich. Aktualnej prezentacji na razie nie zamieszczam, bo nie jest jeszcze gotowa. Niedługo ją dodam, ale muszę w niej wprowadzić sporo technicznych i redakcyjnych zmian. Zwracam uwagę, że w dostępnej poniżej wersji raportu wprowadziłem korekty polegające na prawidłowym użyciu symboli |- i |=. W poprzedniej wersjach pomyłkowo zamieniłem je miejscami. Prawidłowe znaczenia są następujące: |- for — formuła 'for' jest twierdzenie (została udowodniona), |= for — formuła 'for' jest prawdziwa.
Zwracam uwagę, że w nagraniach video nie mogłem oczywiście dokonać tej korekty. Nie dokonywałem jej więc też we wcześniejszych prezentacjach.
Pobierz raport z 2025 09 13