3 ms·

This is great! I wish I had seen something like this years ago. Related: "It's Time for a New Old Language" by Guy Steele. https://www.youtube.com/watch?v=7H

by chubot 9y ago

This is great! I wish I had seen something like this years ago. Related: "It's Time for a New Old Language" by Guy Steele. https://www.youtube.com/watch?v=7HKbjYqqPPQ https://www.youtube.com/watch?v=7HKbjYqqPPQ He gives a history of metalanguage notations (for both language semantics and syntax, including regexes and CFGs). And then he criticizes the inconsistency that has cropped up in these notations over the years. The irony is that people who are formalizing precise semantics of programming languages do not agree on the syntax/semantics of the metalanguage. I guess this is what you notice when you read hundreds of programming language papers, as I'm sure Guy Steele has. ----- Also, does anyone know if what he refers to as "progress and preservation" are the same / related to "liveness and safety" in distributed algorithms? It sounds like the same kind of idea.

neel_k 9y ago
> Also, does anyone know if what he refers to as "progress and preservation" are the same / related to "liveness and safety" in distributed algorithms? It sounds like the same kind of idea. Progress and preservation are used to prove type safety, which (like the name says) is a safety property. Informally, safety means "a bad thing never happens", and liveness means "a good thing will eventually happen". Informally, progress means "a typed program will never immediately exhibit undefined behaviour", and preservation means "a typed program always stays well-typed". Together, these two properties mean "a typed program never exhibits undefined behaviour". This has the shape of a safety property. All this can be made much more formal, but that's the intuition.
mannykannot 9y ago
The inconsistency may be more of a problem for someone new to the field, as it can give such persons the impression that they are not following what the author is saying. With more experience, it is easier to skip over the inconsistencies without really noticing.

by chubot 9y ago

neel_k 9y ago

> Also, does anyone know if what he refers to as "progress and preservation" are the same / related to "liveness and safety" in distributed algorithms? It sounds like the same kind of idea. Progress and preservation are used to prove type safety, which (like the name says) is a safety property. Informally, safety means "a bad thing never happens", and liveness means "a good thing will eventually happen". Informally, progress means "a typed program will never immediately exhibit undefined behaviour", and preservation means "a typed program always stays well-typed". Together, these two properties mean "a typed program never exhibits undefined behaviour". This has the shape of a safety property. All this can be made much more formal, but that's the intuition.

mannykannot 9y ago

The inconsistency may be more of a problem for someone new to the field, as it can give such persons the impression that they are not following what the author is saying. With more experience, it is easier to skip over the inconsistencies without really noticing.