I think this is kinda like the no free lunch theorem—it sounds kinda profound but relies on using the set of all problems/data distributions, which is very OOD from any problem that originates in physical reality.
What examples of practical engineering problems actually have a solution that is harder to verify than to generate?
And I thought uncomputability is only true for programs that don’t halt? A blank program can definitely be verified to halt.
What examples of practical engineering problems actually have a solution that is harder to verify than to generate?
My intuition says that we’re mostly engineering to avoid problems like that, because we can’t solve them by engineering. Or use something other than engineering to ensure that problem is solved properly.
For example most websites don’t allow users to enter plain html. Because while it’s possible to write non-harmful html it’s rather hard to verify that a given piece of html is indeed harmless. Instead sites allow something like markdown or visual editors which make it much easier to ensure that user-generated content is harmless. (that’s example of engineering to avoid having to verify something that’s very hard to verify)
Another example is that some people in fact can write html for those websites. In many places there is some process to try and verify they’re not doing anything harmful. But those largely depend on non-engineering to work (you’ll be fired and maybe sued if you do something harmful) and the parts that are engineering (like code reviews) can be fooled because they rely on assumption of your good intent to work (I think; I’ve never tried to put harmful code in any codebase I’ve worked with; I’ve read about people doing that).
And I thought uncomputability is only true for programs that don’t halt? A blank program can definitely be verified to halt.
For any single program, the question “does this program halt?” is computable, for a trivial reason. Either the program that prints “Yes” or the program that prints “No” correctly answers the question, although we might not know which one. The uncomputability of the halting problem is the fact that there is no program that can take as input any program whatever and say whether it halts.
I think this is kinda like the no free lunch theorem—it sounds kinda profound but relies on using the set of all problems/data distributions, which is very OOD from any problem that originates in physical reality.
What examples of practical engineering problems actually have a solution that is harder to verify than to generate?
And I thought uncomputability is only true for programs that don’t halt? A blank program can definitely be verified to halt.
My intuition says that we’re mostly engineering to avoid problems like that, because we can’t solve them by engineering. Or use something other than engineering to ensure that problem is solved properly.
For example most websites don’t allow users to enter plain html. Because while it’s possible to write non-harmful html it’s rather hard to verify that a given piece of html is indeed harmless. Instead sites allow something like markdown or visual editors which make it much easier to ensure that user-generated content is harmless. (that’s example of engineering to avoid having to verify something that’s very hard to verify)
Another example is that some people in fact can write html for those websites. In many places there is some process to try and verify they’re not doing anything harmful. But those largely depend on non-engineering to work (you’ll be fired and maybe sued if you do something harmful) and the parts that are engineering (like code reviews) can be fooled because they rely on assumption of your good intent to work (I think; I’ve never tried to put harmful code in any codebase I’ve worked with; I’ve read about people doing that).
I endorse this answer.
For any single program, the question “does this program halt?” is computable, for a trivial reason. Either the program that prints “Yes” or the program that prints “No” correctly answers the question, although we might not know which one. The uncomputability of the halting problem is the fact that there is no program that can take as input any program whatever and say whether it halts.