A proof may show that an algorithm works. If the proof is correct*, this may demonstrate that the algorithm is robust. (Though you really want a proof about an implementation of the algorithm, which is a program.)
*A proof that a service will never go down which relies on assumptions with the implication “there are no extreme solar storms” may not be a sufficient safeguard against the possibility that the service will go down if there is an extreme solar storm. Less extremely, perhaps low latency might be proved to hold, as long as the internet doesn’t go down.
How are algorithms made, and how can proofs improve/be incorporated into that process?
Given a problem, you can try and solve it (1). You can guess(2). You can try (one or more) different things and just see if they work(3).
1 and 2 can come apart, and that’s where checking becomes essential. A proof that the method you’re using goes anywhere (fast) can be useful there.
Let’s take a task:
Sorting. It can be solved by:
1. Taking a smaller instance, solving that (and paying attention to process). Then extract the process and see how well it generalizes
2. Handle the problem itself
3. Do something. See if it worked.
2 and 3 can come apart:
At its worst, 3 can look like Bogosort. Thought that process can be improved. Look at the first two elements. Are they sorted? No: shuffle them. Look at the next two elements...
4! = 12, twelve permutations of 4 elements. The sorting so far has eliminated some possibilities:
1, 2, 3, 4
1, 3, 2, 4
1, 4, 2, 3
2, 3, 1, 4
2, 4, 1, 3
Now all that’s needed is a method of shuffling that doesn’t make things less orderly… And eventually Mergesort may be invented.
In the extreme, 3 may be ‘automated’:
programs write programs, and test them to see if they do what’s needed (or a tester gets a guesser thrown at it, to ‘crack the password’)
A proof may show that an algorithm works. If the proof is correct*, this may demonstrate that the algorithm is robust. (Though you really want a proof about an implementation of the algorithm, which is a program.)
*A proof that a service will never go down which relies on assumptions with the implication “there are no extreme solar storms” may not be a sufficient safeguard against the possibility that the service will go down if there is an extreme solar storm. Less extremely, perhaps low latency might be proved to hold, as long as the internet doesn’t go down.
How are algorithms made, and how can proofs improve/be incorporated into that process?
Given a problem, you can try and solve it (1). You can guess(2). You can try (one or more) different things and just see if they work(3).
1 and 2 can come apart, and that’s where checking becomes essential. A proof that the method you’re using goes anywhere (fast) can be useful there.
Let’s take a task:
Sorting. It can be solved by:
1. Taking a smaller instance, solving that (and paying attention to process). Then extract the process and see how well it generalizes
2. Handle the problem itself
3. Do something. See if it worked.
2 and 3 can come apart:
At its worst, 3 can look like Bogosort. Thought that process can be improved. Look at the first two elements. Are they sorted? No: shuffle them. Look at the next two elements...
4! = 12, twelve permutations of 4 elements. The sorting so far has eliminated some possibilities:
1, 2, 3, 4
1, 3, 2, 4
1, 4, 2, 3
2, 3, 1, 4
2, 4, 1, 3
Now all that’s needed is a method of shuffling that doesn’t make things less orderly… And eventually Mergesort may be invented.
In the extreme, 3 may be ‘automated’:
programs write programs, and test them to see if they do what’s needed (or a tester gets a guesser thrown at it, to ‘crack the password’)
evolutionary algorithms