Semantics as observable behavior (was: single-xt approach in the standard)

On 2024-09-22 21:13, Anton Ertl wrote:

Ruvim <ruvim.pinka@gmail.com> writes:

- All standard programs are single-xt programs (in the part of
user-defined words). Why we should remove the way to document this
programs/words in the standard terms of interpretation semantics,
compilation semantics and execution semantics?

 Who proposes removing that?  I often write about the interpretatation
and compilation semantics of various words with default compilation
semantics or with immediate compilation semantics, and I see nobody
who wants to remove that possibility.
 Examples:
 : foo 1 ;
 The execution semantics of FOO are to push 1 on the data stack.
The interpretation semantics of FOO are to push 1 on the data stack.
The compilation semantics of FOO are append the execution semantics of
FOO to the current definition.
 : bar state @ ; immediate
 The execution semantics of BAR are to push the contents of STATE on
the data stack.

Do you agree that this describes an observable behavior, not an implementation?  And all the implementations for execution semantics that show this behavior are observationally equivalent to each other?
For example, this definition:
: bar2  state @ if  state @  else  0  then ; immediate
is observationally equivalent to your `bar`.

The interpretation semantics of BAR are to push the contents of STATE
on the data stack.

I think, we should use the black box model — specify what can be observed. And according to what can be observed, the interpretation semantics of this word are to push zero on the data stack.  *All* implementations for interpretation semantics that show this behavior are observationally equivalent to each other. The same black box argument applies to compilation semantics too.  See bellow.

 The compilation semantics of BAR are to push the contents of STATE on
the data stack.

Anton, forgive me for being blunt, but I think your understanding of "interpretation semantics" and "compilation semantics" for words whose execution semantics depend on STATE is useless both in practice and in theory.
Take a look at my next rationale.
When I'm interested in the interpretation semantics of a word, I'm interested in precisely the behavior that can be *observed* when the Forth text interpreter encounters the name of this word in interpretation state.  And if I specify the interpretation semantics for a word, I specify namely this behavior. And if I want to perform the interpretation semantics for a word, I want to perform namely this behavior. And there are no exceptions to this!
If we say that the term "interpretation semantics" means something else in some cases, we should introduce another term to denote the behavior that can be observed when the Forth text interpreter encounters the name of a word in interpretation state.
But in fact we don't need the term "interpretation semantics" for anything else [1]. Nobody has given any rationale for that.
Then, why do we need to introduce *another* term?  Let us always use the term "interpretation semantics" in exactly this meaning.
The same applies to the term "compilation semantics".

 With that we can then determine what code like
 : bla postpone bar ; immediate
bla .     \ prints 0
] bla [ . \ prints -1
 should do; I show the output in comments.  I just tested gforth,
iforth, SwiftForth, and VFX Forth, and unsurprisingly they all produce
the output shown in the comments.
 

[1] Well, I can see only one reason for using another meaning for the "interpretation semantics" and "compilation semantics" terms than given above: to represent the classic implementation of `postpone` as conforming to what is formally specified in Forth-94, without accepting into the standard the proposed ambiguous condition (see [2]).  But it is better to honestly say that "postpone" appends execution semantics of the word if this word is an immediate word. There is no need to blur the meaning of terms.
[2] https://github.com/ForthHub/discussion/discussions/103#sect.excusing
--
Ruvim