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.)