Co robią projektanci języków, aby zdecydować lub udowodnić, że dana funkcja działa poprawnie?

Interesuję się projektowaniem języka i ogólnie mogę łatwo zrozumieć powszechnie znane cechy (np. Dziedziczenie, polimorfizm, delegaci, lambdy, przechwytywanie, wyrzucanie elementów bezużytecznych, wyjątki, generyczne, wariancje, refleksje itd.), Ich interakcje w konkretny język, sposoby ich ewentualnej implementacji, ich ograniczenia itp.

W ciągu ostatnich kilku miesięcy zacząłem czytać o Rustie, który ma system własności zapewniający bezpieczeństwo pamięci i deterministyczne zarządzanie zasobami poprzez wymuszanie statycznej weryfikacji żywotności obiektów. Z perspektywy zwykłego użytkownika języka mogłem niemal natychmiast podnieść system.

Jednak z perspektywy projektanta języka zajęło mi trochę czasu, aby zrozumieć, dlaczego rzeczy w Rust są dokładnie takie, jakie są. Nie mogłem od razu zrozumieć uzasadnienia niektórych ograniczeń systemu własności, dopóki nie zmusiłem się do wymyślenia przypadków, które naruszałyby integralność systemu, gdyby nie miał tych aspektów.

Moje główne pytanie nie ma nic wspólnego z Rustem i jego własnością, ale jeśli chcesz, możesz użyć go jako przykładu w swoich komentarzach / odpowiedziach.

Kiedy projektanci języków projektują nową funkcję, jakiej metodologii lub procesu używają, aby zdecydować, czy ta funkcja działa poprawnie?

Przez „nowy” rozumiem, że nie jest to coś, co zostało już przetestowane w istniejących językach (a zatem większość pracy została wykonana przez innych projektantów). Przez „działa poprawnie” rozumiem, że funkcja rozwiązuje zamierzony problem poprawnie i jest dość kuloodporna. Przez „w miarę kuloodporny” rozumiem, że żaden kod nie może być napisany w języku lub określonym podzbiorze języka (np. Podzbiór bez „niebezpiecznego” kodu), który naruszałby integralność funkcji.

• Czy jest to proces prób i błędów, w tym sensie, że wymyśliłeś prostą formę funkcji, a następnie próbujesz znaleźć sposoby jej naruszenia, a następnie załatać ją, jeśli skutecznie ją naruszysz, a następnie powtórzyć? A potem, kiedy nie możesz wymyślić żadnych innych możliwych naruszeń, masz nadzieję, że nic nie zostało i nazwać to dniem?

• A może istnieje formalny sposób, aby faktycznie udowodnić (w matematycznym znaczeniu tego słowa), że twoja funkcja działa, a następnie użyć tego dowodu, aby od samego początku upewnić się, że funkcja jest właściwa (lub głównie właściwa)?

(Powinienem wspomnieć, że mam wykształcenie inżynierskie, a nie informatykę. Jeśli więc brakuje mi czegoś, co byłoby oczywiste dla osób z CS, prosimy o zwrócenie uwagi.)

W tej chwili nie mogę znaleźć dokładnego odniesienia, ale jakiś czas temu obejrzałem kilka filmów Simona Peytona Jonesa , który był jednym z głównych autorów projektu Haskella. Nawiasem mówiąc, jest doskonałym mówcą na temat teorii typów, projektowania języka i tym podobnych, a także ma wiele filmów dostępnych za darmo na youtube.

Haskell ma pośrednią reprezentację, która jest zasadniczo rachunkiem lambda powiększonym o kilka prostych rzeczy, aby ułatwić pracę. Rachunek Lambda został wykorzystany i sprawdzony, ponieważ komputer był tylko osobą, która obliczała rzeczy. Ciekawym punktem, o którym często mówi Simon Peyton Jones, jest to, że ilekroć robią coś dzikiego i szalonego z tym językiem, wie, że to zasadniczo dźwięk, kiedy ostatecznie redukuje się do tego pośredniego języka.

Inne języki nie są tak rygorystyczne, co sprzyja łatwości użytkowania lub implementacji. Robią to samo, co inni programiści, aby uzyskać kod wysokiej jakości: przestrzegaj dobrych praktyk kodowania i testuj go na śmierć. Ta funkcja, jak semantyka własności Rust, na pewno wymaga zarówno formalnej analizy, jak i testów, aby znaleźć zapomniane przypadki narożne. Często takie funkcje zaczynają się od pracy magisterskiej.

Tak więc w przypadku projektowania języka istnieją dowody (lub błędy). Na przykład wpisz systemy. Typy i języki programowania to kanoniczna książka opisująca systemy typów i koncentruje się na udowodnieniu poprawności i kompletności systemu typów. Gramatyki mają podobną analizę, a algorytmy (takie jak opisany system własności) mają swoje własne.

W przypadku implementacji językowej jest to kod jak każdy inny. Piszesz testy jednostkowe. Piszesz testy integracyjne. Robisz recenzje kodu.

Jedyną rzeczą, która wyróżnia języki jest to, że są (prawie zawsze) nieskończone. Nie można dosłownie przetestować wszystkich danych wejściowych. I (idealnie) są używane przez mnóstwo ludzi, robiąc dziwne i ciekawe rzeczy, więc w końcu każdy błąd w języku zostanie znaleziony.

W praktyce stosunkowo niewiele języków używa dowodów do weryfikacji ich funkcjonalności i kończy się mieszanką wspomnianych opcji.

Pierwszą i najtrudniejszą rzeczą, którą musi zająć się projektant języka, wprowadzając nowe funkcje, jest utrzymanie spójnego języka:

• jak można go zintegrować z gramatyką języka bez niszczenia istniejącego kodu (można to udowodnić matematycznie)
• jak odnosi się do istniejących funkcji (na przykład, jeśli masz ustawione tablice indeksowane 0..n-1, nie wprowadzisz nowej funkcji zmiennej tablicy indeksowanej 1..n) (to jest część artystyczna projektu)
• jak tę funkcję można wdrożyć w całym łańcuchu narzędzi, aby nowa funkcja mogła zostać wchłonięta przez ekosystem, twórców narzędzi i programistów (wykonalność można wykazać za pomocą koncepcji, ale pełna implementacja jest podejściem podobnym do programowania)

Aby poprowadzić tę sprawę, projektant opiera się na zestawie reguł i zasad projektowania. Podejście to zostało bardzo dobrze opisane w „ Projektowaniu i ewolucji C ++ ” Bjarne Stroustrup , jednej z rzadkich książek poświęconych projektowaniu języka. Bardzo interesujące jest to, że języki rzadko są projektowane w próżni, a projektanci sprawdzają również, w jaki sposób ich języki mają podobne funkcje. Innym źródłem (online i za darmo) są zasady projektowania języka Java .

Jeśli spojrzysz na publiczne postępowanie komitetów normalizacyjnych, zobaczysz, że jest to raczej proces błędu próbnego. Oto przykład na module C ++ całkowicie nowej koncepcji, która zostanie wprowadzona w następnej wersji języka. A tutaj analiza sporządzona po pewnych zmianach językowych , aby ocenić jej sukces. I tutaj proces społeczności Java do definiowania nowych specyfikacji Java, takich jak nowy interfejs API . Przekonasz się, że ta praca jest wykonywana przez kilku ekspertów, którzy twórczo szkicują dokument koncepcyjny i pierwszą propozycję. Następnie propozycje te są weryfikowane przez większą społeczność / komitet, który może je zmienić, aby zapewnić wyższy stopień spójności.

Jak przetestować funkcje języka programowania? To bardzo dobre pytanie i nie jestem pewien, czy stan techniki jest odpowiedni.

Każda nowa funkcja może wchodzić w interakcje ze wszystkimi innymi funkcjami. (Wpływa to na język, dokumenty, kompilatory, komunikaty o błędach, IDE, biblioteki itp.) Czy funkcje łączą się, aby otworzyć lukę? Aby stworzyć nieprzyjemne przypadki krawędzi?

Nawet bardzo inteligentni projektanci języków, ciężko pracujący nad utrzymaniem poprawności tekstu, odkrywają takie naruszenia, jak ten błąd Rust . System typów Rdza nie jest dla mnie tak oczywisty, ale myślę, że w tym przypadku czas istnienia wartości śledzenia ścieżki systemu typów oznacza „podtyp” (podzakresy) w czasie życia koliduje z oczekiwaniami dotyczącymi zwykłego podtypu, koercji, referencji i zmienności, tworząc lukę, w której staticcałe życie ref może wskazywać na wartość przypisaną do stosu, a później stać się wiszącym odniesieniem.

Przez „działa poprawnie” rozumiem, że funkcja rozwiązuje zamierzony problem poprawnie i jest dość kuloodporna.

W przypadku języków, które mają być językami produkcyjnymi , czyli używanymi przez wielu programistów do tworzenia niezawodnego oprogramowania produkcyjnego, „działa poprawnie” musi ponadto oznaczać prawidłowe rozwiązanie zamierzonego problemu dla docelowej grupy odbiorców.

Innymi słowy, użyteczność jest tak samo ważna w projektowaniu języka, jak w innych projektach. Wymaga to (1) zaprojektowania użyteczności (np. Znajomości odbiorców) i (2) testów użyteczności.

Przykładowy artykuł na ten temat to: „ Programiści to ludzie, zbyt , język programowania i projektanci API mogą się wiele nauczyć z dziedziny projektowania czynników ludzkich”.

Przykładowe pytanie SE na ten temat brzmi: Czy przetestowano składnię dowolnego języka programowania pod kątem użyteczności?

W przykładowym teście użyteczności rozważono rozszerzenie funkcji iteracji list (nie pamiętam, który język) w celu pobrania wielu list. Czy ludzie spodziewali się, że będzie się to powtarzać przez listy równolegle lub między produktami? Projektanci języka byli zaskoczeni wynikami testu użyteczności.

Języki takie jak Smalltalk, Python i Dart zostały zaprojektowane z naciskiem na użyteczność. Najwyraźniej Haskell nie był.