Are constructive programs better?

Constructive.idr

import Data.List
import Data.List.Views
import Data.Vect
import Data.Vect.Views

%default total

-- Constructive

rotate : Vect len elem -> Vect len elem
rotate xs {len} with (snocVect xs)
    rotate [] | Empty = []
    rotate (ys ++ [y]) {len=m + S Z} | Snoc z = rewrite (plusCommutative m 1)
                                                in [y] ++ ys
  
-- Proof Carrying

rotate' : (xs : List elem) -> (xs' : List elem ** length xs = length xs')
rotate' xs with (snocList xs)
    rotate' [] | Empty = ([] ** Refl)
    rotate' (ys ++ [y]) | Snoc z = ([y] ++ ys ** rewrite (lengthAppend ys [y]) in 
                                                 rewrite (plusCommutative (length ys) 1) in
                                                 Refl)

-- Separate Proof   
                                         
rotate'' : List elem -> List elem
rotate'' xs with (snocList xs)
    rotate'' [] | Empty = []
    rotate'' (ys ++ [y]) | Snoc z = [y] ++ ys
    
rotate''PreservesLength : (xs : List a) -> (length xs = length (rotate'' xs))
rotate''PreservesLength xs with (snocList xs)
    rotate''PreservesLength [] | Empty = Refl
    rotate''PreservesLength (ys ++ [y]) | Snoc z = rewrite (lengthAppend ys [y]) in 
                                                   rewrite (plusCommutative (length ys) 1) in
                                                   Refl