8 ms·

I suspect most of the CS researchers in the room were, in a sense, lying. I'm going to guess (a) they could all understand the notation if they tried; (b) they

by kapitza 10y ago

I suspect most of the CS researchers in the room were, in a sense, lying. I'm going to guess (a) they could all understand the notation if they tried; (b) they were in fact taught the notation in some undergraduate class, math camp, etc, etc; and (c) what happened is that they intentionally forgot it. At least, this is the case for me! I think one of the dirty secrets about the CS distaste for many areas of math, including conceptual areas like category theory that are in fact quite closely related to computing and directly applicable there, is that when judged as CS, they don't seem like very good CS. For example, a programming-language designer who uses symbols that aren't on any keyboard deserves to be laughed out of the room. What are these weird 19th-century squiggles? I see what you're doing, sort of, but why are you doing it? This is obviously a petty example. But computer scientists, at least ones with a certain kind of systems background, have put a lot of work into designing abstract logical structures for human beings to use. They've learned a lot of rules about how to do this well. The corpus of pre-CS math that gets applied to CS doesn't seem to care about any of these rules. It takes a lot of work to come up with a CS aesthetic, and when you have one, your brain only has room for "good" systems that play by your rules. If a system doesn't map to your rules, it's almost physically painful to have to contemplate it. Practicality is not quite the issue. TLA+ seems to be a very useful thing and Lamport has produced a large, large, body of extremely useful work. At the same time, I can't help feeling it would be neat if someone did for TLA+ what Ousterhout did for Paxos.

tedsanders 10y ago
Of course, the alternative hypothesis is that they weren't lying and they did forget it. As someone who majored in math quite successfully within the last decade, I can honestly tell you I didn't remember what ":" meant and therefore had trouble parsing the expression. I don't think I forgot intentionally or was lying.
- gizmo686 10y ago
  As someone currently majoring in mathamatics, I can honestly say this is the first time I have seen ":" used in this way. The "standard" way I would expect to see that would be for the first ":" to be replaced with a "|", and the second one to be replaced with a "," (or omitted entirely). The third ":" does not look out of place, although I would probably omit it, or right it as "st". EDIT: for clarity, I would right the set as: "{f : [1..N ⟶ 1..N] | ∀ y ∈ 1..N , ∃ x ∈ 1..N st f[x]=y}" The ":" in this case indicates that f has the indicated type. As long as I am commenting on my sense of "standard" notation, I should also note that the "[1..N ⟶ 1..N]" notation also seems weird (as in, I have never seen it before). I would expect it to be written as [1..N] ⟶ [1..N]. Perhaps replacing [1..N] with Z_n for the appropriate audience; however the speaker seems to be aware that this is a strange notation, as he commented about it in the beginning. In this particular case, I would probably also omit the entire predicate in favor of writing "onto" above "⟶", which I can do because the particular property being described is common enough to have a name; however this would defeat the point of showing the notion. Once I have entirely omitted the predicate like this, I would probably omit naming f entirely, giving the notation {[1..N] ⟶ [1..N]} (again, with "onto" written above the arrow). Actually, depending on audience, in this particular case I would replace the entire set with either "The symmetric group of order n", "The symmetric group S_n", or just "S_n". The f[x] notation looks a bit weird out of context, but does come up when the distinction between a function and a function application is important (often times f(x) is used as a convention to remind the reader that f is a function)
  - pron 10y ago
    Lamport wrote it the way he did because that's the TLA+ notation, and the talk was about TLA+. That formula is actually parsed by the TLA+ tools. Unlike paper math, TLA+ needs to have a precise grammar. I'm really not sure why `|` isn't used in set comprehensions, but I'm guessing that he wanted to keep `:` as "such that" everywhere. `f[x]` is used b/c round parentheses are reserved for operator arguments, and functions aren't operators (the whole thing is based on axiomatic set theory, and in formal math "function" must be something very specific).
nabla9 10y ago
>east ones with a certain kind of systems background, have put a lot of work into designing abstract logical structures for human beings to use. They've learned a lot of rules about how to do this well. This is very arrogant and wrong. The exact opposite is true. Mathematicians have worked hundreds of years and streamlined notations that can express complect things well.
- theoh 10y ago
  There are bad notations in mathematics, and I think there may well be some truth in the idea that designing for usability is more important in CS. Your comment is needlessly rude and you don't give any evidence to support your contention.
  - nabla9 10y ago
    I was insulting his argument, not the person. If his argument is offended, I apologize. I don't think it's possible.
    - deleted 10y ago
      [deleted]
- deleted 10y ago
  [deleted]
- corndoge 10y ago
  I am a mathematics student working as a systems software engineer. I find mathematical notation excessively dense and tedious to interpret. Given the expression: {f ∈ [1..N ⟶ 1..N] : ∀ y ∈ 1..N : ∃ x ∈ 1..N : f[x]=y} I can instantly read it in my head as: The set of all f where f is a function mapping 1..N to 1..N such that for all Y in 1..N there exists an X in 1..N such that f[x] = y. One might argue that the ability to express such a long definition in such a compact form is a benefit, but I don't think so. In this particular case the definition is so trivial that it's easy to understand what is being talked about. Anything more complicated than this quickly becomes tedious and boring. I would prefer that mathematicians simply used longer, more verbose, but more clear and explanatory names for quantities and concepts. Just my opinion, though.
fataliss 10y ago
This! Exactly this! Honestly as a CS person I might be completely biased but, I often hear this quote around the office "The hardest part of software engineering is naming things". We spend a lot of time and effort to name things in a way that a non engineer would understand. I wish people in hard sciences would do the same. I often times understand the underlying concepts described by all these Greek letters and symbols but it gets lost in translation. That is why I love efforts like https://betterexplained.com/ https://betterexplained.com/ where math is made concrete.
- Retra 10y ago
  I was a mathematician and physicist before I went into CS, and when you're doing all your writing on paper and chalkboards, you don't want to write 'code' at all.
- mannykannot 10y ago
  To name something well you have to understand it, and maybe that is the hard part of naming.
  - foota 10y ago
    This interestingly gets into the common fantasy magic concept of names having power over something. (perhaps this is also a thing in past cultures?)
    - eternalban 10y ago
      The games got it from "past cultures".
    - yolesaber 10y ago
      The idea of names as power comes from pre-unified Ancient Egypt in which (i may have gotten the kingdoms mixed) the upper kingdom's religious rituals included the use of secret and ceremonial names known to only an elite literate cabal. From there the religion developed to include aspects of secret names for anything and everything and religious texts indicated that people believed once they learned something's secret name they would be able to exert control over them. In fact, most of the concepts one associates with 'magic' (sigils, astronomical connotations, power words) derive from the Ancient Egyptian religion. See Wallace Budge's "Egyptian Magic" for an excellent treatment on the subject. His book has tons of direct primary source examples that are very entertaining (people turning into crocodiles, priests trying to shape the outcome of wars by creating effigies, lots of fun stuff)
Chinjut 10y ago
As a mathematician/(ex?-)computer scientist whose area of research is category theory, let me ask: What makes category theory not seem like very good CS?
- mannykannot 10y ago
  Apparently, the first thing is the difficulties it presents for typing. I think that is about all we need to know about this argument.
  - Chinjut 10y ago
    For what it's worth, it does bother me how much standard CS tooling and the mindset bred from it is stuck in the paradigm of exclusively textual user interfaces. Linear text has its advantages and value, of course, but, like, we know well by now that not everything is best thought of or manipulated this way; that diagrams and other modes of communication and interaction can be useful. (This has nothing to do with why I'm interested in category theory [it's not that my motivating goal in life was to draw commutative diagrams…], but it's a somewhat relevant thought to the discussion I've had all the same. We as computer scientists talk a lot about trees, and graphs, and this structure, and that structure, and also about human computer interaction, and the importance of design, and yet the only structure we allow ourselves expression via at the end of the day is text, text, text.)
    - mannykannot 10y ago
      A lot of people draw informal sketches while thinking things through, and there have been waves of enthusiasm for formalizing such things, but except in a few specialized cases (e.g. state transition diagrams) nothing so far seems to have proved useful enough to really take off. I do wonder sometimes if we are too focused on computer languages, to the detriment of tools (see also Animat's comment.)
    - TheOtherHobbes 10y ago
      God yes. Text and lack of imagination are the two curses of CS.
inimino 10y ago
> they intentionally forgot it. I'm not sure intentionally forgetting something is even possible, but, who would intentionally forget something foundational? Most computer scientists do study math and generally wish they knew more, not less.
troydj 10y ago
Yes, agreed! You'd think most of the CS people in a room listening to a Lamport lecture, of all things, would've at some point in their education taken a theory of computation or similar course. The notation Lamport was asking about is already taught by page 7 of chapter 0 in Sipser [1]. [1. https://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/113318779X https://www.amazon.com/Introduction-Theory-Computation-Micha...]
deleted 10y ago
[deleted]
eximius 10y ago
This is hilarious to me. I have always found notation used outside of math hideous. Compare any math notation to the notation used in operational semantics or proving things about type environments. Compare any math notation to the logic notation used in philosophy. Hideous, all hideous, I say!
- lake99 10y ago
  > Compare any math notation to the logic notation used in philosophy. Aren't they the same? I assume that by "logic notation used in philosophy" you mean the kind that's used by Carnap, Kripke, etc.
  - dpc59 10y ago
    Logic in philosophy is used in a lot of fields of humanities and social sciences too. When you have inductions and deductions based on qualitative axioms what you write is going to take a lot of brainpower to understand. A lot of the academic work in those fields takes thousands of words to explain all the thinking behind something that could be broadly explained in a paragraph.
    - lake99 10y ago
      No, I don't think this is what eximius was talking about. I think the kind you're talking about does not use any symbolic notation.
  - eximius 10y ago
    Admittedly, my exposure was brief and I certainly don't know the notation by any name, but the logic courses used drastically different notation from what I was used to in my math classes. Some of the symbols were the same, sometimes they had the same meanings, sometimes not. Often there were different symbols entirely.
j2kun 10y ago
> But computer scientists, at least ones with a certain kind of systems background, have put a lot of work into designing abstract logical structures for human beings to use. They've learned a lot of rules about how to do this well. You say this like mathematicians haven't been doing this for thousands of years.
- dpc59 10y ago
  They didn't build their system for it to work with computers.
  - j2kun 10y ago
    > designing abstract logical structures for human beings to use Moreover, you do realize that computers were invented by mathematicians, right?

by kapitza 10y ago

tedsanders 10y ago

Of course, the alternative hypothesis is that they weren't lying and they did forget it. As someone who majored in math quite successfully within the last decade, I can honestly tell you I didn't remember what ":" meant and therefore had trouble parsing the expression. I don't think I forgot intentionally or was lying.

gizmo686 10y ago
As someone currently majoring in mathamatics, I can honestly say this is the first time I have seen ":" used in this way. The "standard" way I would expect to see that would be for the first ":" to be replaced with a "|", and the second one to be replaced with a "," (or omitted entirely). The third ":" does not look out of place, although I would probably omit it, or right it as "st". EDIT: for clarity, I would right the set as: "{f : [1..N ⟶ 1..N] | ∀ y ∈ 1..N , ∃ x ∈ 1..N st f[x]=y}" The ":" in this case indicates that f has the indicated type. As long as I am commenting on my sense of "standard" notation, I should also note that the "[1..N ⟶ 1..N]" notation also seems weird (as in, I have never seen it before). I would expect it to be written as [1..N] ⟶ [1..N]. Perhaps replacing [1..N] with Z_n for the appropriate audience; however the speaker seems to be aware that this is a strange notation, as he commented about it in the beginning. In this particular case, I would probably also omit the entire predicate in favor of writing "onto" above "⟶", which I can do because the particular property being described is common enough to have a name; however this would defeat the point of showing the notion. Once I have entirely omitted the predicate like this, I would probably omit naming f entirely, giving the notation {[1..N] ⟶ [1..N]} (again, with "onto" written above the arrow). Actually, depending on audience, in this particular case I would replace the entire set with either "The symmetric group of order n", "The symmetric group S_n", or just "S_n". The f[x] notation looks a bit weird out of context, but does come up when the distinction between a function and a function application is important (often times f(x) is used as a convention to remind the reader that f is a function)
- pron 10y ago
  Lamport wrote it the way he did because that's the TLA+ notation, and the talk was about TLA+. That formula is actually parsed by the TLA+ tools. Unlike paper math, TLA+ needs to have a precise grammar. I'm really not sure why `|` isn't used in set comprehensions, but I'm guessing that he wanted to keep `:` as "such that" everywhere. `f[x]` is used b/c round parentheses are reserved for operator arguments, and functions aren't operators (the whole thing is based on axiomatic set theory, and in formal math "function" must be something very specific).

nabla9 10y ago

>east ones with a certain kind of systems background, have put a lot of work into designing abstract logical structures for human beings to use. They've learned a lot of rules about how to do this well. This is very arrogant and wrong. The exact opposite is true. Mathematicians have worked hundreds of years and streamlined notations that can express complect things well.

theoh 10y ago
There are bad notations in mathematics, and I think there may well be some truth in the idea that designing for usability is more important in CS. Your comment is needlessly rude and you don't give any evidence to support your contention.
- nabla9 10y ago
  I was insulting his argument, not the person. If his argument is offended, I apologize. I don't think it's possible.
  - deleted 10y ago
    [deleted]
deleted 10y ago
[deleted]
corndoge 10y ago
I am a mathematics student working as a systems software engineer. I find mathematical notation excessively dense and tedious to interpret. Given the expression: {f ∈ [1..N ⟶ 1..N] : ∀ y ∈ 1..N : ∃ x ∈ 1..N : f[x]=y} I can instantly read it in my head as: The set of all f where f is a function mapping 1..N to 1..N such that for all Y in 1..N there exists an X in 1..N such that f[x] = y. One might argue that the ability to express such a long definition in such a compact form is a benefit, but I don't think so. In this particular case the definition is so trivial that it's easy to understand what is being talked about. Anything more complicated than this quickly becomes tedious and boring. I would prefer that mathematicians simply used longer, more verbose, but more clear and explanatory names for quantities and concepts. Just my opinion, though.

fataliss 10y ago

This! Exactly this! Honestly as a CS person I might be completely biased but, I often hear this quote around the office "The hardest part of software engineering is naming things". We spend a lot of time and effort to name things in a way that a non engineer would understand. I wish people in hard sciences would do the same. I often times understand the underlying concepts described by all these Greek letters and symbols but it gets lost in translation. That is why I love efforts like https://betterexplained.com/ https://betterexplained.com/ where math is made concrete.

Retra 10y ago
I was a mathematician and physicist before I went into CS, and when you're doing all your writing on paper and chalkboards, you don't want to write 'code' at all.
mannykannot 10y ago
To name something well you have to understand it, and maybe that is the hard part of naming.
- foota 10y ago
  This interestingly gets into the common fantasy magic concept of names having power over something. (perhaps this is also a thing in past cultures?)
  - eternalban 10y ago
    The games got it from "past cultures".
  - yolesaber 10y ago
    The idea of names as power comes from pre-unified Ancient Egypt in which (i may have gotten the kingdoms mixed) the upper kingdom's religious rituals included the use of secret and ceremonial names known to only an elite literate cabal. From there the religion developed to include aspects of secret names for anything and everything and religious texts indicated that people believed once they learned something's secret name they would be able to exert control over them. In fact, most of the concepts one associates with 'magic' (sigils, astronomical connotations, power words) derive from the Ancient Egyptian religion. See Wallace Budge's "Egyptian Magic" for an excellent treatment on the subject. His book has tons of direct primary source examples that are very entertaining (people turning into crocodiles, priests trying to shape the outcome of wars by creating effigies, lots of fun stuff)

Chinjut 10y ago

As a mathematician/(ex?-)computer scientist whose area of research is category theory, let me ask: What makes category theory not seem like very good CS?

mannykannot 10y ago
Apparently, the first thing is the difficulties it presents for typing. I think that is about all we need to know about this argument.
- Chinjut 10y ago
  For what it's worth, it does bother me how much standard CS tooling and the mindset bred from it is stuck in the paradigm of exclusively textual user interfaces. Linear text has its advantages and value, of course, but, like, we know well by now that not everything is best thought of or manipulated this way; that diagrams and other modes of communication and interaction can be useful. (This has nothing to do with why I'm interested in category theory [it's not that my motivating goal in life was to draw commutative diagrams…], but it's a somewhat relevant thought to the discussion I've had all the same. We as computer scientists talk a lot about trees, and graphs, and this structure, and that structure, and also about human computer interaction, and the importance of design, and yet the only structure we allow ourselves expression via at the end of the day is text, text, text.)
  - mannykannot 10y ago
    A lot of people draw informal sketches while thinking things through, and there have been waves of enthusiasm for formalizing such things, but except in a few specialized cases (e.g. state transition diagrams) nothing so far seems to have proved useful enough to really take off. I do wonder sometimes if we are too focused on computer languages, to the detriment of tools (see also Animat's comment.)
  - TheOtherHobbes 10y ago
    God yes. Text and lack of imagination are the two curses of CS.

inimino 10y ago

> they intentionally forgot it. I'm not sure intentionally forgetting something is even possible, but, who would intentionally forget something foundational? Most computer scientists do study math and generally wish they knew more, not less.

troydj 10y ago

Yes, agreed! You'd think most of the CS people in a room listening to a Lamport lecture, of all things, would've at some point in their education taken a theory of computation or similar course. The notation Lamport was asking about is already taught by page 7 of chapter 0 in Sipser [1]. [1. https://www.amazon.com/Introduction-Theory-Computation-Michael-Sipser/dp/113318779X https://www.amazon.com/Introduction-Theory-Computation-Micha...]

deleted 10y ago

[deleted]

eximius 10y ago

This is hilarious to me. I have always found notation used outside of math hideous. Compare any math notation to the notation used in operational semantics or proving things about type environments. Compare any math notation to the logic notation used in philosophy. Hideous, all hideous, I say!

lake99 10y ago
> Compare any math notation to the logic notation used in philosophy. Aren't they the same? I assume that by "logic notation used in philosophy" you mean the kind that's used by Carnap, Kripke, etc.
- dpc59 10y ago
  Logic in philosophy is used in a lot of fields of humanities and social sciences too. When you have inductions and deductions based on qualitative axioms what you write is going to take a lot of brainpower to understand. A lot of the academic work in those fields takes thousands of words to explain all the thinking behind something that could be broadly explained in a paragraph.
  - lake99 10y ago
    No, I don't think this is what eximius was talking about. I think the kind you're talking about does not use any symbolic notation.
- eximius 10y ago
  Admittedly, my exposure was brief and I certainly don't know the notation by any name, but the logic courses used drastically different notation from what I was used to in my math classes. Some of the symbols were the same, sometimes they had the same meanings, sometimes not. Often there were different symbols entirely.

j2kun 10y ago

> But computer scientists, at least ones with a certain kind of systems background, have put a lot of work into designing abstract logical structures for human beings to use. They've learned a lot of rules about how to do this well. You say this like mathematicians haven't been doing this for thousands of years.

dpc59 10y ago
They didn't build their system for it to work with computers.
- j2kun 10y ago
  > designing abstract logical structures for human beings to use Moreover, you do realize that computers were invented by mathematicians, right?