The issue is there to verify a program you need to have a spec. To generate a spec you need to solve the general problem.
This is what gets swept under the rug whenever formal methods are brought up.
This is what gets swept under the rug whenever formal methods are brought up.
For example, many things can be proven about the following program without having to solve any general problem at all:
echo “hello world”
Similarly for quick sort, merge sort, and all sort of things. The degree of formality doesn’t have to go to formal methods which are only a very small part of the whole field
Congratulations, you just launched all the worlds nuclear missiles.
This is to spec since you didn't provide one and we just fed the teletype output into the 'arm and launch' module of the missiles.