Poczytałem sobie książkę o programowaniu na listach, dokładniej o języku LISP. Podejście niestandardowe, dosyć bliskie moim zachciankom. Zacząłem testować to podejście w praktyce i zaczęło się!
Przebudowanie funkcji, które zmieniają się dynamicznie w czasie działania programu - zapewnione niemalże gratis. Mogą nawet powstawać i być usuwanymi. Zwrot wielu wartości naraz, przepraszam, co znaczy wartość. Wszystko, co jest umieszczone na listach istnieje, niepotrzebna im jakaś tam wartość. Ona może co najwyżej służyć jako dodatkowe pole.
Zajrzałem do zwykłej logiki z tym podejściem. Dowód formalny, zwłaszcza twierdzenie o dedukcji upraszcza się tak bardzo, że po wprowadzeniu listy założeń i ich przebudowie za pomocą reguły odrywania nie ma co robić. Wystarczy tylko sprawdzić, czy wyrażenie dowodzone znajduje się na liście.
I dodatkowa niespodzianka, kiedy wyrażenie musi korzystać z jakiegoś dodatkowego założenia o przestrzeni, lista wskaże tylko wszystkie prawdziwe przypadki!
Przy dowodzie prawa Dunsa Scota mam założone tylko istnienie oraz brak jednego zdania. Nie dowiodę innego, chyba... że przestrzeń jest zupełna, oraz prawda i fałsz są jedynymi możliwościami! Słowem rewelacja. Od razu wykryte ukryte założenia, o których normalnie się nie wspomina. Konstruktywizm w pełnej krasie. Na razie to pierwsze spojrzenie, ale im wiecej wzorów dowodzę w ten sposób, tym bardziej mi się to podoba.
