There are two aspects of correctness:
one is internal consistency, so that whatever you define can be assigned a
proper meaning. Typically, that is why you are told that the domains
you use must be CPO, so that you can have limits used to defined the
semantics of some looping/recursive construct, whether program or data.
the other is consistency with you intended semantics. This is a
general problem with specification of program, or languages or
anything else. When you design something, the correctness of your
design can only be checked with respect to some reference, and in
this case formal reference. I develop this second point.
If a child ask you for a car with 4 wheels. You may buy him a small
automobile, and be in agreement with the specification. But what he
actually wanted was a new passenger car for his train, and the child
will be unhappy. The specification is incomplete (or incorrect) and as a consequence
the end result may not adequate.
So a specification may not exactly reflect your intent. You can prove
that your realisation of a car (or your compiler) is conformant with
specification, but you have no way to prove that your specification is
conformant with whatever intent is in your mind.
The denotational semantics of a language is a specification of the
language, and you have no way to prove that it conforms what is in
your mind, unless you can express that formally, which will just be
annother specification, of which you are not sure it conforms your
However, if you make your intent more precise in several different
ways, you can check that your various attempts at specifying what you
want are consistent, which will give you greater belief that what you
are doing conforms what you want. But there is no way to be certain.
For example, you can attempt to prove the consistency of your
denotational semantics with another formal specification or semantic
definition, as suggested in your question. These specifications do not
have to be complete specifications. It may only be a statement of some
property of your language.
Consistency with previous version of the language
Still, in your case, there is something that you may do, that you should do.
The language you are considering is an extension of another language,
that may have a formally defined semantics.
Then one thing that users will expect is that the extended language
will work like the original one when the new features are not used.
Hence, one thing you should prove is that any program of the original
language is given the same semantics in the new language.
It may be however that there has been some changes so that
programs have to be adapted for the new extended version of the language. Then
if you can formally defined how program P for the original language is
to be tranformed into another program P' in the extended language, then
you ideally should prove that this tranformation is semantics preserving.
If such a tranformation of programs to the new language version is necessary, and not clearly obvious, it may be worth defining semantics of the original language (if it does not exist yet) in order to prove the correctness of the transformation.
I have to disagree with Kaveh's answer main statement that
The point of formal semantics is that we take the class of
mathematical structures that we want to study and map it to another
class of mathematical structures that we already know something
about, and we use that knowledge to study the original class of
The problem is that, in general, we have no mathematical structure to
begin with. At best we have a syntax, defining sentences in a
language. The first point of formal semantics is to associate a
meaning with sentences (programs) following this syntax, and do it
formally so that we can study this meaning and prove properties about
it. So the semantics is indeed taking syntactic sentences to a class
of mathematical structures theat we are supposed to understand. But
We are not interested in studying the syntax, which is the only
original structure that is being mapped. We may have an intuitive
meaning in mind, but it can hardly be the domain of a mathematical
We are indeed interested in studying our intended meaning for programs
though the mapping of the syntax that expresses them into semantics.
But the mapping applies only to the syntax, not to the intended
meaning we hope to study ... if the semantics we define does conform
What we may do, though, is take two mapping from the same syntactic
structure into different classes of mathematical stuctures, and prove
the existence of a mapping between these structures, with properties
that represent some form of consistency of the two definitions.