Would it be possible to create a Turing complete programming language, where the result of a program always includes a easy to verify proof that the result is valid. Let me explain in more details.
Lets say that any program P of this programming language takes an input x and produces an output (y, p) where y is the normal output of the program and p is a proof that P(x) = y. Obviously, validating this proof should not consist in just rerunning the program but should be possible without doing so (ideally in linear time).
I would for now assume that all operations of the programming language are deterministic and no user inputs or similar things are allowed.
In addition, I would also allow as proof one that is just having a very high probability of being true.
If it is not possible to create such a language why?