Given a sorted array and a value we know is in it, why can we know for sure that if we search it in linear order starting at the beginning, we will eventually always find the value at some index?

Because we know it will. How would having a proof of that help a programmer?

but the mythical algebra could be built on simple theorems like this, much like Eucledian geometry, and then expanded to cover deeper and more meaningful theorems.

When someone shows me how math can help me write code to deal with

1. interferance from an unseen lift motor in the building next door, that only happens on Teusday mornings(*), at one installation site out of 300, that causes my serial port server to loose data.

   *Because that's when the shop next door took delivery of it's peanuts, which being very dense meant it was easy to overload the freight lift and cause the motor to arc.

2. Or defend against the correct data being supplied in the wrong units.
3. Or users entering "VISA" in the field labelled "name on the card".
4. Or a 4GB XML file with mismatched tags.

Math theorems tend to only work under very specific sets of assumables, which real-world code rarely enjoys.