On Thu, 10 Aug 2017 07:48:34 +0200, Borneq
<b...@a...hidden.pl> wrote:
> Czepiasz się powiedzenia a nie odnosisz się do meritum.

Nie czepiam się. Po prostu jest to przysłowie ludowe, które być może
nijak ma się do faktów. Warto czasem przemyśleć.


> Automatyczne sprawdzanie poprawności to "święty Graal" informatyki.

Nie. Święty Graal to przenośność.


> Co prawda udowodniono matematycznie że nie może istnieć maszyna
Turinga
> sprawdzająca poprawność innej maszyny Turinga,

Jest gorzej: udowodniono że nie da się udowodnić aksjomatów. Patrz
twierdzenie Goedela.

(Genialne jest że Goedel wymyślił digitalizację twierdzeń w czasach
gdy nie było komputerów.)


> Javie stosuje się system asercji czy unit testy, w C++ jest
biblioteka
> GSL i odpowiedni plugin sprawdzający zgodność z

Trochę mylisz pojęcia. Asercje nijak nie są automatyczne, bo jak ich
nie napiszesz, to ich nie masz. (W swoim kodzie.) Podobnie testy
jednostkowe - nie sprawdzają czy wynik jest poprawny, ale tylko czy
jest zgodny z oczekiwaniami - i tak samo trzeba je napisać.

Zapomniałeś (?) o lint i innych podobnych, np. PMD. Zapomniałeś o
sprawdzaniu składni w trakcie edycji.

> A Rust wymusza swoje reguły. Trudno początkującemu w Rust jest
wręcz
> nieraz dla pewnych przypadków napisać kod który się skompiluje (te
> problemy z mutualnością) ale to jest wymuszone automatycznie, nie
musi
> tego sprawdzać programista i czegoś przeoczyć.

To trochę brzmi jak idealny język dla biurokratów. Wszystko jest
wymuszone, zgodne ze standardami i procedurami, jedynie słuszne.

W latach 70-tych były dwa modne języki programowania: C i Pascal.
Pascal znacznie lepiej sprawdza to co uznaje za poprawność. C ma
filozofię "róbta co chceta". Cytując klasyka "grzeczne panienki idą
do nieba, niegrzeczne tam gdzie chcą".

Obecnie Pascal w pierwotnej formie nie jest używany. Jest jakieś
Delphi, jest Lazarus z FPC. Natomiast klasyczne C trzyma się całkiem
dobrze, a nawet przeżywa drugą młodość na MCU.