I don't think it's arbitrary value attribution that's going on here
From what I understood, this is not attributing randome numeric values to the developer specs, consumer specs and code itself then peforming some algebra to say "see, it results in 42 so therefore, it does what you asked.
It's possible I'm out to lunch but I'm reading this as mathmatical proof that the program logic does not do anything it's not designed to do; the anomolies have been ironed out. When you have a random program crash currently, the developer mostly guesses at the cause and in some cases may never track down the issue. In such a case with this suggested analysis, you would know exactly where that random crash occured and why because it would fall outside of the mathmatical proof. I see it as a tool removing buffer overflow and any other programmer error resulting in those obscure exploitable results.
As it stands now, we can exploit software to perform tasks it was not intended to do. In this possible future, software would be produced at such a level of quality that exploting anomolies in the program logic to get an unintended result would not be possible.
