> Zwlaszcza pisanie programow ktorych poprawnosc jest niemozliwa do
> zwryfikowania. "Templates" to skomplikowana forma makrogeneratora
> ktora przeksztalca program w 'cos" co dopiero jest kompilowane. W co -
> pzreksztalca? Nie wiadomo, i trzeba meic 100 procentowe zaufanie do
> calej maszynerii ze a) przeksztalca zgodnie z intencja programisty, b)
> przksztalca bez bledow.

Ad b) I do tego się dąży. Powstaje kompilator compcert (co prawda tylko
do podzbioru C), który formalnie dowodzi, że semantyka programu została
zachowana po optymalizacji.

Co do C++, formalna weryfikacja nie jest możliwa, m.in. dlatego, że
w standardzie są błędy logiczne -
http://gallium.inria.fr/~xleroy/publi/cpp-constructi
on.pdf

w.