What to prove and how to prove it
I think you raise an important point, which is that in a high level language, specifications can be hard to distinguish from implementations. For example, in Coq, the specification of "The sum of the elements of a list of naturals" is probably going to look something like:

Fixpoint sum (l : List Nat) : Nat :=
  match l with
   | [] =&gt; 0
   | x::xs =&gt; x + sum xs


It's hard to imagine what the specification of this would be, other than some predicate like

 Inductive Is_Sum : Nat -&gt; List Nat -&gt; Prop :=
    | IS_Empty : Is_Sum 0 []
    | IS_Cons : Is_Sum s xs -&gt; Is_Sum (x + s) (x::xs)


which really just seems like a re-formulation in terms of logic programming. Indeed it is very easy to show forall l : List Nat, Is_Sum (sum l) l.

At this point, it is indeed possible to test the definition of sum and make sure it lines up with our intuition, e.g. check sum [1,2,3] = 6. However, there is an important other step we can check in terms of "specification checking", that of proving derived properties. For sum, we could prove

Proposition sum_append : forall l1 l2, sum (l1 ++ l2) = sum l1 + sum l2


or

Proposition sum_leq : forall l x, In x l -&gt; x &lt;= sum l


These propositions establish the consistency of our definition against some of our intuitions, and avoid certain silly mistakes, e.g. if we had returned $1$ instead of $0$ for the empty list.

Indeed, often for our purposes the properties we actually are interested are the derived properties! Defining the full specification is only a means to an end, like strengthening the induction hypothesis.

Finally, it's probably useful to note that in real life, our specifications are often much simpler than our implementations! Indeed, if our implementations are doing nothing clever, then why do we care so much about proving them correct? (well, actually even the simplest of programs might benefit from proofs.)

One rather simple example is merge sort which while pretty straight forward, is certainly complex enough to warrant a proof of correctness, and at any rate is very different looking than its specification.