I'm a big believer in spiral learning, and think that it's absolutely ok to teach younger kids algorithms without proof of correctness with hand-wavy motivations, in order to get them used to the idea and feel empowered in using the algorithms, and then to come back to the proof later, once they have more mathematical maturity.

But yes, teaching additional non-arithmetic algorithms would probably be very useful; two related examples I like are binary search in a dictionary and lexicographic ordering to make your own dictionary/index. This can then also lead to an investigation of sorting algorithms, and then back to math.

> prove correctness

They would have to know induction which appears in 9th(?) grade algebra. Efficiency analysis would likely be super difficult even to high school students.