> Não se pode garantir que um programa vá terminar (sair pelo "exit" ou pelo > "stop") em nenhuma situação, pois para se garantir um teste completo de um > programa o mais trivial possível, por exemplo um programa que le dois > numeros do teclado, faz a soma e imprime o resultado, teríamos que testar > para todos os nueros possíveis, o que é, obviamente, impossível.
Não necessariamente. É possível utilizar prova matemática envolvendo intervalos. Por exemplo, eu sei sempre que 'x+x' = '2x', para qualquer 'x' real. E para isso não preciso percorrer todo o conjunto dos reais (infinito) para provar que isto é uma tautologia. Naturalmente, a dificuldade/inviabilidade da prova cresce à medida que o programa torna-se mais complexo. ++Neste caso vc prova a sentença, mas ao construir o programa vc cai nas limitações físicas (processador, memória, intervalo de números representáveis (range), tipos, etc.) Se a linguagem for "fortemente tipada" temos operações comportadas, entre tipos iguais ou equivalentes, mas em uma linguagem onde o tipo não é previamente definido/amarrado à variável.........