Let's say there's a cloud computing service that allows people to run arbitrary programs and get the results. The idea being that your machine is too slow, and you don't want to overwhelm it. If your program is something like "factorize 15672965357291016", then it's a perfect candidate for this service, because you can very quickly verify that a result handed back to you is correct. But if your program is long and complicated, and you can't think of a quick way to verify that a given input/output pair is correct, then you're stuck with running the program on your own machine to verify the results, which defeats the purpose.
One solution would be to use the blockchain and have a lot of people verify that some given input/output pair is correct--then you only accept the result as true when whatever block it's on has enough confirmations. The problem with this is that it could really slow down the network if your program is resource-intensive.
What would be nice to have is a programming language where a given program
P, an input to it
I, and a supposed output
O, can be verified quickly (i.e.
P(I) == O). That way, making confirmations would be fast, and the whole network would speed up.
I don't think this can be done in general because you could use it to solve the halting problem. If you have some function
V(P, I, O), which verifies that
P(I) == O, then running
V(P, I, halts) would check that
P halts on input
However, the fact that
V does exist for every problem in
NP makes me think that there has got to be some middleground, where you could make a really restricted language for which
V always exists, and it can easily be determined from the structure of
P (a trivial implementation is just
V(P, I, O) = P(I) == O). I'm not really sure what my question is, but is this an existing problem? What search terms should I use to learn more about this?