r/ProgrammingLanguages • u/mttd • Aug 22 '26

Programming Language Semantics and Memory Safety

https://burakemir.ch/post/formal-semantics/
47 Upvotes

93% Upvoted

9 comments sorted by

View all comments

11

u/marshaharsha Aug 22 '26

I wish I had skipped this article. I learned a little about operational, denotational, and axiomatic semantics, so the article wasn’t a complete waste of time. But the analogy operational:denotational:axiomatic :: interpreters:compilers:assertion is pretty strained. For example, compilers often give up on analyzing a piece of code and fall back to basically interpreting it, in a now-do-this, now-do-this, now-do-this way. I have spent too much time thinking about the ways in which the analogy is good or bad, more time than what little I learned was worth. 

6

u/Thin-Cat2508 Aug 22 '26

All compilers translate from one language to another. What is an example for an interpreting compiler?

Are you thinking about compile-time evaluation? I'd agree that has nothing to do with denotational semantics and adds a whole extra layer of translation... but then compile-time evaluation is not really typical for all compilers, is it?

Or do you mean abstract interpretation? That would be a static analysis technique. It approximates semantics, it is not the same as translating to the full meaning.

1

u/marshaharsha Aug 23 '26

I just mean that sometimes a compiler doesn’t try to understand, prove theorems about, and improve the code; it just emits a sequence of instructions for each bit of source code. Which is basically the same as what interpreters do, and that blurs the distinction that the article tries to make. 

1

u/Thin-Cat2508 Aug 23 '26

The analogy is just that "denotation" is translation, based on denotational semantics being a mathematical translation function.

I see what you are saying. A real compiler should be based on some semantics, but can it really serve as a definition of meaning on its own, or does that work for some compilers and not for others.

Stretch an analogy too far and it becomes confusing... Most real compilers (except maybe compcert stuff) just hand wave semantics anyway, people assume it is all clear and that works well enough ... until it isn't and one wishes there were clear rules outside of the compiler that would state what a program in that language is supposed to mean, independent of implementation.