How to go about proving an algorithm correct?
To prove the correctness, we have to prove actually the function
rmax(x,y) returns the the maximum number with index between x and
y in the array S[1..n], provided the hypothesis: 1≤x≤y≤n.

There is a semantic technique that often works nicely for recursively
defined functions such as this one.

Your function can be defined as the least fixed-point of a functional:

F = λ rmax, x, y. if y-x≤1 then max(S[x],S[y]) else
                  else max(rmax(x,(x+y)/2), rmax((x+y)/2+1,y))


I have changed a bit the style, for convenience. You note that F is a
function of 3 arguments, and you original function rmax is defined
as its least fixpoint in the semantic domain. Also, here rmax is a local name for the first argument of F. I could replace it by any other name (alpha conversion). I kept rmax only for readability.

Now, the way you prove correctness is by checking that this
functionnal preserves correctness when it is applied to a function
foo that is correct, when it is defined (it is undefined for example
if it does not terminate, but being defined is actually a formal
semantic property).

That is, you only have to check that if the function foo(x,y) is correct, then
the function F(foo) is also correct.

F(foo) = λ x, y. if y-x≤1 then max(S[x],S[y]) else
                 else max(foo(x,(x+y)/2), foo((x+y)/2+1,y))


When y-x≤1, we know that either x=y or x=y-1, since by
hypothesis 1≤x≤y. In both cases we see that max(S[x],S[y]) is the
right answer.

Otherwise, we see that 1≤x≤(x+y)/2≤n and 1≤(x+y)/2+1≤y≤n. Hence the
hypothesis is verified for the two calls to the function foo. So,
since the function foo is correct by hypothesis, each call (when
giving a defined result) returns the maximum array value between the
bound given by its parameters (if it is defined). Since both ranges
cover the range between x and y, the maximum of these two values
is the maximum value between x and y.

Note that there is no base case in this recursion. The reason is that
it starts using with the totally undefined function $\bot$ (read "bottom"), which is
thus always correct when it is defined.

Note that this does not prove termination of the algorithm. But you get that easily by induction.

Some further explanations.

This proof is in a way very similar to the proof suggested by Yuval
Filmus. It is not too surprising as they are both supposed to prove
the same result. However they are quite different in spirit. Yuval's
proof is a recursion on the steps of an actual interpretation of the
program (operational semantics). The proof I am proposing is by
recursion on the structure of the program code seen as an infinite
program defined as the limit of an infinite sequence of finite program
(denotational semantics). It assumes continuity properties (so that
passing to the limit makes sense), which are verified for usual
computing operations and predicates.

The former proof is on the use of the program, while the latter is on its structure.