I’m not sure I agree with this. Programming languages have a defined semantics that can be demonstrated by executing the code. With mathematical notations, you’re left reading the text to understand exactly what the notation is meant to express.

You are confusing “executable” with “semantics.” Most programming languages do not have a defined semantics, even though they are executable. Notably, Standard ML does have a defined semantics. It’s the only example of a non-research language that I know of with one, though I’m sure there are more out there.

The best example to illustrate why this is true is by thinking about compilation. The source code of a compiled language is not executed, it is translated into an executable language. How do you know that there is not a bug in the compiler? Well, you don’t, because the semantics of the language is generally not defined, so the de facto semantics becomes however the compiler is implemented. For more on that particular subject, I suggest reading Concrete Semantics, my favorite book on the subject. It shows, among other things, how to prove that a compiler preserves the semantics of the source program. This involves defining exactly, unambiguously what programming language semantics means.

With mathematical notations, you’re left reading the text to understand exactly what the notation is meant to express.

This explains the confusion - mathematic notation is unambiguous, and has clear, defined semantics. That’s how it can be the basis of reasoning for our society. A set in set theory means something very specific. Quantification of variables means something very specific. You can trace meaning all the way down to the axioms, it is a fully open and defined system. You cannot “execute” set theory, which is what you might mean, but ironically, our executable code does not have explicit semantics, whereas our mathematics does.

No, most programming languages have a defined semantics, although not formally defined. In general any language where it’s possible to write multiple implementations that agree have a defined semantics.

As to “only ml and research languages have formal semantics”, scheme is intended as a production language; SPARK is explicitly a production language.

I’m having trouble understanding your conclusion, which is that an informal semantics is somehow more descriptive than formal semantics.

most programming languages have a defined semantics, although not formally defined

This means that instead of having an unambiguous formal semantics to reference, when implementing a language you have to use inaccurate, informal, and context-dependent descriptions probably written in a communication language like English. So your statement:

With mathematical notations, you’re left reading the text to understand exactly what the notation is meant to express.

I find to be describing informal semantics. Informal means you have to provide an interpretation of the semantics, because there is no unambiguous interpretation of them. With math / formal logic, you actually don’t need to read the semantics in any way, since they are machine-checkable. So I feel like your conclusion is the reverse of what’s true: informal semantics makes interpretation more difficult. Formal semantics brings clarity and removes ambiguity, by definition.

You also misread what I said about languages with formal semantics. I specifically said that there are probably other languages out there that I don’t know about with formal semantics. At least, my intention was not to say that Standard ML is the only one, just the only one that I could think of off the top of my head:

It’s the only example of a non-research language that I know of with one, though I’m sure there are more out there.

I’m not sure I agree with this. Programming languages have a defined semantics that can be demonstrated by executing the code. With mathematical notations, you’re left reading the text to understand exactly what the notation is meant to express.

I’m unable to read the article. But I will note that there

areexecutable languages that aren’t “programming languages”, strictly speaking.There is a recorded talk available as well.

You are confusing “executable” with “semantics.” Most programming languages do not have a defined semantics, even though they are executable. Notably, Standard ML does have a defined semantics. It’s the only example of a non-research language that I know of with one, though I’m sure there are more out there.

The best example to illustrate why this is true is by thinking about compilation. The source code of a compiled language is not executed, it is translated into an executable language. How do you know that there is not a bug in the compiler? Well, you don’t, because the semantics of the language is generally not defined, so the de facto semantics becomes however the compiler is implemented. For more on that particular subject, I suggest reading Concrete Semantics, my favorite book on the subject. It shows, among other things, how to prove that a compiler preserves the semantics of the source program. This involves defining exactly, unambiguously what programming language semantics means.

This explains the confusion - mathematic notation is unambiguous, and has clear, defined semantics. That’s how it can be the basis of reasoning for our society. A set in set theory means something very specific. Quantification of variables means something very specific. You can trace meaning all the way down to the axioms, it is a fully open and defined system. You cannot “execute” set theory, which is what you might mean, but ironically, our executable code does not have explicit semantics, whereas our mathematics does.

No, most programming languages have a defined semantics, although not formally defined. In general any language where it’s possible to write multiple implementations that agree have a defined semantics.

As to “only ml and research languages have formal semantics”, scheme is intended as a production language; SPARK is explicitly a production language.

I’m having trouble understanding your conclusion, which is that an informal semantics is somehow more descriptive than formal semantics.

This means that instead of having an unambiguous formal semantics to reference, when implementing a language you have to use inaccurate, informal, and context-dependent descriptions probably written in a communication language like English. So your statement:

I find to be describing informal semantics. Informal means you have to provide an interpretation of the semantics, because there is no unambiguous interpretation of them. With math / formal logic, you actually don’t need to read the semantics in any way, since they are machine-checkable. So I feel like your conclusion is the reverse of what’s true: informal semantics makes interpretation more difficult. Formal semantics brings clarity and removes ambiguity, by definition.

You also misread what I said about languages with formal semantics. I specifically said that there are probably other languages out there that I don’t know about with formal semantics. At least, my intention was not to say that Standard ML is the only one, just the only one that I could think of off the top of my head: