>>> My preference for using a well-defined convention based on some 
>>> existing markup language is that the text is then plain ASCII (and 
>>> hence easy to type and to display) but we can additionally prettify it 
>>> in a reliable way if the user cares about it.
>>
>> The GNU preferences are described in standards.texi, and we should 
>> follow them, not our personal preferences.
>
> Does standards.texi offer advice on how to format Emacs Lisp comments, 
> or does it otherwise contradict anything that Stefan M wrote?
>

AFAICS, it doesn't.  Here is the 5.10 Quote Characters section of the GCS:

In the C locale, the output of GNU programs should stick to plain ASCII 
for quotation characters in messages to users: preferably 0x22 (‘"’) or 
0x27 (‘'’) for both opening and closing quotes. Although GNU programs 
traditionally used 0x60 (‘`’) for opening and 0x27 (‘'’) for closing 
quotes, nowadays quotes ‘`like this'’ are typically rendered 
asymmetrically, so quoting ‘"like this"’ or ‘'like this'’ typically looks 
better.

It is ok, but not required, for GNU programs to generate locale-specific 
quotes in non-C locales. For example:

printf (gettext ("Processing file '%s'..."), file);

Here, a French translation might cause gettext to return the string 
"Traitement de fichier ‹ %s ›...", yielding quotes more appropriate for a 
French locale.

Sometimes a program may need to use opening and closing quotes directly. 
By convention, gettext translates the string ‘"`"’ to the opening quote 
and the string ‘"'"’ to the closing quote, and a program can use these 
translations. Generally, though, it is better to translate quote 
characters in the context of longer strings.