Ur/Web doesn't redefine “correctness”, since, by definition, your program specification is the definition of what it means for your program to be “correct”. Ur/Web merely guarantees the absence of certain behaviors in programs written in it.