Odnoszę się tutaj do pytania: potężne algorytmy zbyt złożone, aby je zaimplementować .
Jeśli algorytm jest potężny, ale zbyt skomplikowany, aby go wdrożyć, skąd możesz mieć pewność, że algorytm jest poprawny? Bez implementacji nie będzie można przetestować algorytmu w scenariuszu ze świata rzeczywistego, a tak złożony algorytm może zawierać błędy, które mogą unieważnić algorytm.
Tego nie rozumiem; jeśli masz techniki, aby udowodnić poprawność algorytmu, to algorytm już go implementuje, prawda? Albo w jaki sposób możemy być pewni, że technika sprawdzania jest poprawna?
Przepraszam, jeśli zabrzmi elementarnie!
Aktualizacja z Kaveha (odtworzona tutaj, ponieważ argument jest lepszy!):
Jeśli możesz formalnie udowodnić poprawność algorytmu w systemie formalnym, takim jak Coq, możesz również wyodrębnić algorytm (ponieważ zasadniczo zaimplementowałeś algorytm), ale kluczowym faktem jest to, że w przypadku większości algorytmów nie dajemy formalnych dowodów potwierdzających poprawność algorytmu, używamy nieformalnych dowodów poprawności. Dowody mogą być fałszywe, co zdarza się od czasu do czasu, a nawet formalny dowód poprawności nie zapewni nam absolutnej pewności, że algorytm jest poprawny.