Has the notion of "non-cheating" quines been formalised?

Informally, it is often said that some quines "cheat", such as those that read their own source code from memory, or the case where a program consisting of the empty string happens to output the empty string.

Quines that are considerd to be "non-cheating" always seem to have the same structure. There is some data structure (usually, but not always, a string) which contains some representation of the source code. This structure is read twice, once to reformat it into the code part of the final output, and a second time where it's copied verbatim to reproduce the data part. For example, the following Python example (which I just invented) has this structure:

x = """x = {0}{1}{0}
print x.format(chr(34)*3,x)"""
print x.format(chr(34)*3,x)

The string 'x' is referred to twice in the last line, once to reformat it, and a second time to paste it verbatim into the reformatted string.

My question is whether this notion of "cheating" or "non-cheating" quines has been, or can be, formalised. That is to say, if we are given a formal specification of a language and its semantics, and we are also given an example of a quine in that language, is there a well-defined way to say, in principle, whether that quine is "cheating" or not? Or is this notion of "cheating" inherently too vague to admit a formal definition?

If this notion can be formally defined, is it possible to have a language that only admits "non-cheating" quines, and is an example of such a language known?

Most formal semantics for programing languages tend to keep things simple, in particular, it's pretty rare to have the ability to express "grabbing your own source code" in a formal semantics.

This has the somewhat dubious advantage of disallowing some kinds of "cheating" by construction: the "cheat" is simply not part of the language semantics. In particular, a simple lambda calculus with simple string concatenation and printing primitives cannot implement many (any?) of the "cheats" you have in mind. In such a language, a quine might be a program which prints the exact string representation of it's own code. You can even avoid the print primitive if you allow returning the string rather than printing it. In that case, you only need string literals and concatenation.

It's a useful exercise to figure out various properties of quines in such a language. It's pretty easy to see that some variable will need to be repeated twice: there are no "linear" quines. However the statement


This structure is read twice, once to reformat it into the code part of the final output, and a second time where it's copied verbatim to reproduce the data part.

is a bit vague, and I'm not sure it's true in general, depending on the precise meaning of "copied verbatim".

StackExchange Computer Science Q#62742, answer score: 2