4 ms·

Short answer: no. Long answer: https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_

Short answer: no. Long answer: https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_... There cannot be a program that can prove (or even help a human to prove) any true statement about programs written in a Turing-complete language.

bsaul 9y ago
As always with this theorem it's pretty hard to be sure if the kind of non provable statement happen often enough to be a concern in practice
hackinthebochs 9y ago
But most code isn't using the features that make Turing complete languages messy, i.e. evolving the executable code as executing progresses. Most real-world code exists in a subset of Turing complete languages where generic theorem proving could probably work.