Streszczenie (autorskie):

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 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 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.
Niestety w żadnym z obu obszarów nie dopracowano się metod, które weszłyby na stałe do repertuaru narzędzi inżynierii oprogramowania. Wreszcie zaniechano tych badań, co autorzy mo-nografii 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 od 1949 roku tego 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 po-prawnoś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 przedstawię pewną nową propozycję podjęcia problemu poprawności pro-gramów, a także wyjaśnię, dlaczego wymaga to „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ę moją książkę (w stanie surowym) „Denotacyjna inżynieria języków programowania”, którą mogę udostęp-nić w wersji cyfrowej. Z jej wydaniem na razie się nie spieszę, by zebrać jak najwięcej opinii czytel-ników. I oczywiście, za wszelkie takie opinie będę niezmiernie wdzięczny.

Streszczenie autorskie:

In this talk, I will report on the ongoing work on coreference analysis in a multilingual context. I will present two approaches in the analysis of coreference and coreference-related phenomena: (1) top-down or theory-driven: here we start from some linguistic knowledge derived from the existing frameworks, define linguistic categories to analyse and create an annotated corpus that can be used either for further linguistic analysis or as training data for NLP applications; (2) bottom-up or data-driven: in this case, we start from a set of features of shallow character that we believe are discourse-related. We extract these structures from a huge amount of data and analyse them from a linguistic point of view trying to describe and explain the observed phenomena from the point of view of existing theories and grammars.

Tłumaczenie streszczenia:

Podczas wykładu opowiem o trwających pracach nad analizą koreferencji w kontekście wielojęzycznym. Przedstawię dwa podejścia do analizy zjawisk koreferencyjnych: (1) teoretyczne, gdy na podstawie wiedzy lingwistycznej definiujemy kategorie językowe i używamy ich do stworzenia anotowanego korpusu, który można wykorzystać albo do dalszej analizy lingwistycznej, albo jako dane treningowe dla zastosowań NLP, (2) oparte na danych: w tym przypadku zaczynamy od zestawu płytkich cech naszym zdaniem związanych z dyskursem, wyodrębniamy struktury z dużej ilości danych i analizujemy je z językowego punktu widzenia próbując opisać i wyjaśnić obserwowane zjawiska za pomocą istniejących teorii i gramatyk.