I used to work on formal specifications and program proofs, around the time Lamport was developing temporal logic. I took the position that, rather than trying to make programmers learn math, we should automate and divide up the problem so that they didn't have to.[2][3] This meant minimizing the formalism and making the verification information look like ordinary programming. It also meant carving out the harder math problems into a separate system where someone using a theorem prover would prove the necessary theorems in a way which allowed their use and reuse by ordinary programmers. The underlying math is still there, but not in your face so much.

There's a mathematician mindset: Terseness is good. Cleverness is good. Elegance is good. Generality is good. Case analysis is ugly. This is unhelpful for program verification.

Program verification generates huge numbers of formulas to be proven. Most of the formulas are very dumb, and can be dealt with automatically by a simple theorem prover. Where it's necessary to prove something hard, our approach was to encourage users to write more assertions in the code to narrow the thing to be proven, until they were down to "assert(expra); assert(exprb);" Getting to that point is much like ordinary debugging.

Now they just needed a theorem, independent of the program, that could prove "exprb" given "expra". That job could be handed off to a theorem-proving expert. A library of proved and machine-checked theorems would be built up. Some would be general, some project-specific. This is the software engineer's approach to the problem.

The mathematician's approach is to capture much of the program semantics in mathematical form and work on them as big math formulas. Most of the work is done in the formula space, where mathematicians are comfortable, not the code space, where programmers are comfortable. This seems to hold back the use of formal methods in program verification.

Much effort has gone into trying into trying to find some clever way to make program verification elegant. "A great variety of program logics are in use in computer science for the specification of (software and/or hardware) systems; for example: modal and temporal logics, dynamic logic, Hoare logic, separation logic, spatial logic, nominal logic, lax logic, linear logic, intuitionistic type theory, LCF."[4] We used to call this the "logic of the month club".

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/bo... [2] http://www.animats.com/papers/verifier/verifiermanual.pdf [3] http://portal.acm.org/citation.cfm?id=567074 [4] http://homepages.inf.ed.ac.uk/als/PSPL2010/

   logic of the month club

We have known since the stone age (of computing) that we can reason about any computation using e.g. ZFC set theory, since we can formalise the operational semantics of any computation in ZFC. The problem is that general purpose logics like ZFC are extremely inefficient (in the sense of having too large a proof search space). For example ZFC allows you to reason about statements like: 4 \in squareroot(3). But such questions are meaningless in reasoning about programs. ZFC is too expressive. What all the work on program logics is about is to find logics that are 'more efficient'. That means they should be

(1) Expressive enough to enable reasoning about program propertise that we care about.

(2) Make the proof search space as small as possible.

(3) Make specification and reasoning convenient (for computer or programmer).

All the logics you mention make some progress towards these goals. Nominal logic for example makes reasoning about programs with binders more efficient. Separation logic makes reasoning about stateful computation more efficient. Type theories are progress towards integrating programming, specification and proving (whether that's desirable or not is a contentious question). The LCF approach gave use the currently dominant interactive theorem prover architecture. Linear logic has been the single most influential idea in the last 3 decades in the design of typing systems, especially for concurrent systems.

   write more assertions

More precisely, how do I engage in the dark incantations required to conjure up my own proven methods? For my critical code, right now I just write unit tests. Do you know some place that can shed some light as to what I actually do? I mean, I can just tell my coworkers "yea I formally proved this, it won't have bugs" but I don't think that's quite in good spirit.

To be able to state that a piece of software is bug-free and formally correct, we first need a notion of correctness: that the algorithm follows a [formal] specification.

The first step would be to formally specify what the software/algorithm should do. Then, the next step would be to use formal methods and mathematical tools (e.g. set theory and logic) to prove that your algorithm does exactly as the specification says.

TLA+ is a formal method that can be used for writing specifications and model-checking them. While a big step forward from testing, model-checking still doesn't "prove" anything.

For proving, you can use theorem provers like the Z3 [0] SMT solver (or a formal framework that uses theorem provers) to do proof checking.

The Event-B [1] method is one such formal method that uses SMT solvers and allows you to model systems starting with a very abstract and high-level model, state invariants about your system, and prove that those invariants hold as you refine your models and make them more concrete.

Feel free to shoot me an email if you like to talk more about formal methods :)

[0]: https://github.com/Z3Prover/z3

[1]: http://www.event-b.org/

VST: http://vst.cs.princeton.edu/

Dafny: http://rise4fun.com/Dafny/tutorial

You are probably not going to get to the point of being able to tell your coworkers "yes, this is formally verified" unless you are working in a specific domain where you have few/no libraries and very clearly stated and well trusted assumptions about the external environment (hardware, etc).

It's not going to be mission critical but it'll be nice to flash and say "I used formal methods to prove this implementation" as it is going to be for an academic's project.

Unfortunately, there aren't great deductive verification tools for either Python or JavaScript.

Perhaps more importantly, there's also not a particularly good understanding of how to formally verify front-end code.

The most important property of a visualization system is something like "the visualization accurately represents the data being visualized", but in a problem domain like this, formalizing the high-level intent is probably harder than actually proving that this intent is achieved.

Additionally, the cost of throwing an exception at runtime are presumably pretty low (unlike in a control system, for example). So once you've formalized your spec, you can just check your specs at run time throw an exception/report a bug instead of or in addition to generating the possibly faulty visualization.

Are there key components of the visualization pipeline that could threaten its correctness? E.g. data reduction, interpolation, fancy graphics code, etc.? If so, I'd focus on those and come up with a good set of formal, checkable-at-runtime contracts that capture your high-level informal specification.

Alternatively, is it possible to do some computation on your output to check that it matches the input data? E.g. you could imagine counting pixels of certain colors on a heat map or pie chart and comparing that to the original data. That way you don't have to verify (or trust) all of the graphics generation code, thus significantly reducing your trusted computing base.

Saying "we have a formal mathematical description of what it means for this portion of the visualization system to be correct, and a way of checking input/output matches that description" is probably a more significant contribution than actually churning through a static verification effort.

> it'll be nice to flash and say "I used formal methods to prove this implementation" as it is going to be for an academic's project.

Are you sure this is the case? Most academics, even within CS, don't care much about formal methods.

If you're just looking to learn formal methods, then I guess it's whatever. But if you're looking to stand out, you might want to figure out what's important to your stake holders and focus on that. I'd be pleasantly surprised if the answer to that question is formal methods.

> If you're just looking to learn formal methods, then I guess it's whatever. But if you're looking to stand out, you might want to figure out what's important to your stake holders and focus on that. I'd be pleasantly surprised if the answer to that question is formal methods.

I was just joking around a bit. I've been interested for some time.

I think the first time I truly appreciated the power of ∀ and ∃ was during functional analysis when I found myself juggling an overwhelming number of different notions of continuity, convergence, smoothness and the like. ∀ and ∃ drew out the subtle distinctions that the blurry, imprecise words of the English language conspired to hide. They let me break down logic hairballs completely indigestible to my mammalian intuition into small chunks that I could individually process. Same idea as algebra.

That's their purpose, and they're very good at it. Nothing I've encountered in the world of programming languages really comes close to doing their job. Don't fall in to the trap of assuming they're pointless just because they don't apply to your problems.

On the other hand, in MathLand we have conventions like saying "2x" when you want to multiply x by 2, but if you write "dx" you'd better know if you're doing calculus or not, because it means something totally different depending on context.

Mathematical notation is pretty squishy. There are probably thousands of uses of every greek letter and their italic, bold and variously curlicue'd isomorphs. And it's mostly culture, with a lot of history, personalities and land-grabs thrown in. You can't necessarily crack open a paper without a lot of baggage-level context ("Oh yeah, this community uses brackets for things that community uses subscripts for, okay...")

On the other hand, C++ is complicated and messy and also mostly a train wreck, but at least there's a standard you can go read.

[I once thought it would be worthwhile to learn denotational semantics. The "at least one new hijacked hieroglyph must appear on every page" nature of the reading put me off it in short order. I had no idea where to start interpreting the notation other than maybe attending a class to get the proper starter culture. It was frustrating to see notation go in the "squishy" direction when I thought it should have been using something you could parse and run tools against. Oh well.]

More than anything, I think this is the main reason why studying many subfield of mathematics is so difficult, when we spend more time and effort in things like parsing instead of in the actual subject matter.

Even popular subjects may show similar problems. For example, in Sedgewick's Analysis of Algorithms, he gives the following common definition:

> O(f(N)) denotes the set of all g(N)....

In the next page, he presents an exercise:

> Show that f(N) = N lg N + O(N) implies f(N) = ϴ(N log N)

Reader looks at that "N lg N + O(N)" and tries to make sense of the addition of a number to a set of functions. Note, this is in page 5, so many readers unfamiliar with the culture of the area are likely to just abandon the book (and perhaps the study of the subject) as they could not translate to themselves the very first formula presented by the author.

The only clue to anything that could help the newbie to get some answers lies in a couple of references that point to the historical uses of these greek symbols for computational complexity. Within that reference [1], by no other than Knuth, one can find the explanation for such syntax:

> "1+O(n^-1) " can be taken to mean the set of all functions of the form 1+g(n), where |g(n)| < Cn^-1 for some C and all large n.

And then he goes on about the problem of that syntax in respect to one-way equality:

> we write 1+O(n^-1) = O(1) but not O(1) = 1+O(n^-1). The equal sign here really means ⊆ "set inclusion", and this has bothered many people who propose that we not be allowed to use the = sign in this context. My feeling is that we should continue to use one-way equality together with O-notations since it has been common practice of thousands of mathematicians for so many years now, and since we understand the meaning of our existing notation sufficiently well.

The above is not only a reason for logicians to laugh at the pretense that mathematical language is formal, but also an example of things that are likely not to be in books but in an unwritten culture of a field.

--

[1] - Knuth, Big Omicron and big Omega and big Theta

This is a great comparison!

It's automata and computational theory 201, not parody

This notation is not for relaying the concept of permutations, for that (good) mathematics textbooks would simply write this explanation in plain English.

What the notation is good for is manipulating the notion of a permutation in a greater context, e.g. when you want to show that the functional composition of two permutations is itself a permutation, you can just replace this verbal description with the formal notation, shuffle around the symbols a bit, until you arrive at something that is obviously true.

Try doing that using the verbose English description.

Isn't that the point of any DSL? Also, wasn't the advent of DSLs meant to make it easier for non-programmers to understand the flow of control in a system?

I think generally the idea was to make things easier to understand by factoring out the complicated bits (implementation) and leveraging abstraction to provide clarity on top of an implementation.

If this is the case for every DSL I and every other CS major designs, why should it not be the goal of every math major? Sure to you and many other math-centrist people these symbols are "how I learned it so it must be the best" but to everyone else it's difficult to grasp and hard to understand.

The lingo is half the battle for most things but for math it seems like the lingo is the entire battle.

There's a kernel of truth there.

To abuse the DSL metaphor further, even mildly complicated mathematics concepts are only expressible using layer upon layer of ever-more-abstracted DSLs. Lower-level expansions of the building blocks to improve clarity for reading would be useless in practice, since mathematics is intended to be written and understood by humans and such an expansion would exceed our ability to keep the entire intended concept in our working memory.

Proficiency in mathematics is proficiency with understanding and extending the lingo itself. Mathematics /is/ the lingo, which is why it can't be unraveled from it.

>"how I learned it so it must be the best"

Not at all. It is, however, a very practical approach to getting someone up to speed to be able to do actual mathematics (as opposed to the basic symbol manipulations that most people confuse with actual mathematics.)

You cannot just black box everything away and choose to ignore it the way programmers do with source code and libraries.

The metric for success with a program is "does the machine run it properly". The metric for success with a piece of mathematics is "do people who've done some reading in my field understand my new result". You can cheat in one but not in the other.

That's just plain incorrect. I expect all code to be written to standards of which would allow anyone to read.

> Mathematics is built based on understanding all the concepts behind a subject, and it's written to express to another human clear rigorous thought.

Isn't abstraction designed to avoid this? To remove a solution from a problem domain? To work on it without integral knowledge of all; applications? If not then all of Computer Science has been doing it wrong.

> You cannot just black box everything away and choose to ignore it the way programmers do with source code and libraries.

We don't do that. We black box things that aren't related to the problem at hand by referring to them in a terse and understandable way. For instance if I want to use a fork join scheduler for parallel thread scheduler I don't need to write out all the code for a fork join scheduler. I just need to say "You probably know what this is, if not it's called a fork join scheduler and I'll interact with it via sending messages of run, runAll, etc" and be done with it. I wont use an obscure Greek letter to notate a Fork-Join as that's archaic and insane.

> The metric for success with a program is "does the machine run it properly". The metric for success with a piece of mathematics is "do people who've done some reading in my field understand my new result". You can cheat in one but not in the other.

The KPIs for software are as follows: functionality, maintainability, simplicity. In that order. There is no single goal of software but instead a multifaceted set of goals constantly working against each other yet CS people make room for an even balance.

I don't see how this relates to you engaging in proving further information from other information. I don't see why math needs 40 non-terminal characters to type out a proof. I don't see why it can't be written in a way that is more approachable while not detrimental to the performance of current professionals. I also find it unfathomable that someone would think that the current way of doing things is the, all together, best way of doing things because that points a blind eye at the other two things I mentioned: "maintainability, simplicity".

I wouldn't call any of the advanced math world "simple" or "maintainable".

So you only work on open source hardware, with open source operating systems and open source drivers and open source software? And you've read the code for the libraries you use of course? Please. Unless you're Stallman you're not really assessing how much black boxing you are actually doing.

>We don't do that. We black box things that aren't related to the problem at hand by referring to them in a terse and understandable way. For instance if I want to use a fork join scheduler for parallel thread scheduler I don't need to write out all the code for a fork join scheduler. I just need to say "You probably know what this is, if not it's called a fork join scheduler and I'll interact with it via sending messages of run, runAll, etc" and be done with it. I wont use an obscure Greek letter to notate a Fork-Join as that's archaic and insane.

You do do that. And have you ever really read any mathematics at all? It is literally exactly what you describe. "I am going to use a fiber bundle here, I'll call it (A,B,pi,F), you probably know what this is..." I guess you just hate Greek? The notation is terse and completely obvious to anyone who has the faintiest idea about the mathematics they are reading. Letters are not used to describe abstract ideas (these have English names) they are used to express specific variables. Just like you do in CS. It's hard to type 'alpha' on an English keyboard or programmers would call things alpha as well. The letter notation is essential to express your ideas clearly. The subject material in doing advanced mathematics is much more difficult, abstract and complex than writing code usually, so the notation looks more difficult. That's all.

It isn't simple. Because what it's describing isn't simple. It is maintainable because it's easy to read once you understand it. Understanding is the hard part.

Programmers always think they can "fix math" by swapping notation around. They don't realize that it's as good as it can be until they actually start doing some real mathematics. Notation is really not a problem. It's a tiny minimal bump along the road that massively simplifies the entire endeavor and tries to get out of the way of actually understanding the mathematics, which is the difficult part.

The only objection you're raising that has merit is that a lot of the symbols aren't on a keyboard. Which is why we have TeX. Which is the digital language of mathematics. \pi is really not hard to type.

And operating system is an operating system. A database is a database. A text editor is a texteditor.

I don't need to know exactly how someone's solution is implemented to understand the concepts and I've written at least one piece of toy software that does everything I do on a day to day. I've done CPU graphics rendering, GPU graphics rendering, web parsing, low level kernel/OS stuff, a lot of things. I'm not an expert. I'm still a student and as such I am and always will be learning. That doesn't mean I'm not a Computer Scientist and that doesn't mean I can't open up documentation on any part of my entire system and get a working facsimile from the ground up. Not to say it will be as performant of course (now that I'm in a computer organization course I can just now realize how horrible my scribbles of a CPU I wanted to build is. No pipelining and everything was going to be hooked up to a huge bus).

Basically, yes anything computer related is something I can sit down and make work. Hardware or software I can design something that will probably work to a degree. Will it work well? No. Will it be the exact same implementation as someone else? Of course not. Will my implementation function the same as whatever I'm replacing? Absolutely.

The black boxing is made in such a way that with basic documentation you can construct in your mind how said box may function.

> I guess you just hate Greek?

No I just like standard keyboard keys.

> The notation is terse and completely obvious to anyone who has the faintiest idea about the mathematics they are reading

The key here is "who has the faintiest idea about the mathematics they are reading". It's not meant for outsiders. It's meant for an in-group. Not for anyone who want's to learn math.

> Just like you do in CS. It's hard to type 'alpha' on an English keyboard or programmers would call things alpha as well

Not anyone who would ever work for, or with, me. I'd replace that code in a hot minute. Anything past a toy you're never going to ever use again NEEDS more then "alpha" or "a". Naming is the most important thing in CS, the runner up is abstraction.

No one worth their salt would ever seriously use single letter variable names outside of maybe the following list:

   i, j: Loop variables. Holdovers from FORTRAN.
   x, y: Talking about a position in a matrix or in space. 

> The subject material in doing advanced mathematics is much more difficult, abstract and complex than writing code usually, so the notation looks more difficult. That's all.

Oh so it's just that mathematics is hard and computer science is easy. That makes sense.

This elitism is part of the issue. I think mathematics is hard but I've worked on many complicated projects and they all don't really seem complicated. We work as a field to tame complexity through understanding a problem domain and abstracting the unimportant implementation details.

It all just turns into operations on data that are (sometimes) sequential. No matter if it is data processing and rendering for an oscilloscope like system, optimizing networking protocols and writing your own stack over UDP to control ordering of packets that are non-essential, or even writing huge orchestration systems that operate on generated statistical models to predict future actions that need to be taken. The simplistic comes from an understanding of how to create interfaces for the complex that are simpler then what they are representing.

> It isn't simple. Because what it's describing isn't simple. It is maintainable because it's easy to read once you understand it. Understanding is the hard part.

It seems like most of the time, when a colleagues explains something to me, I can completely understand the concept but I have no time for the fodder of inefficient notations that are adored by mathematicians.

> Programmers always think they can "fix math" by swapping notation around.

I hardly think I can "fix math". I want someone to fix math so I can learn it and then join in on the party. I want to learn it. It's just overly complicated.

> They don't realize that it's as good as it can be until they actually start doing some real mathematics

You're crazy if you think the current way of doing things cant be improved. Improvements are always happening in my field and I learn and adapt as they they are brought to me. Mathematicians have been stuck with an attitude of "it's different and I don't like it".

> It's a tiny minimal bump along the road that massively simplifies the entire endeavor and tries to get out of the way of actually understanding the mathematics, which is the difficult part

For you it's a tiny bump. For someone who is attempting to learn out of the classroom for their own interests it's the only difficult part. I can go to khan academy and learn about pretty much any college level topic. When I go to take a class at my college (I need to take 3 math courses) I can't learn anything. So much archaic nonsense and a lack of good explanations for new comers.

> The only objection you're raising that has merit is that a lot of the symbols aren't on a keyboard. Which is why we have TeX. Which is the digital language of mathematics. \pi is really not hard to type.

Pi tells you it's a variable, Pi does not tell you why it's a variable. I have no idea how to convey that meaning as I am not in the "cool kids club" that you and your colleagues have built for yourself

Mathematics is for experts that have mastered the lower levels of the abstraction layer. You cannot study any subfield of math without having understood the basic definitions of the field. No amount of syntax rewriting is going to change that; those definitions are not going anywhere.

What I'd expect to follow here would be a statement about how your abstractions should be terse and verbose in the right ways. Terse in the implementation specific handling and verbose in the explanation of your abstract solution.

"Software is for experts that have mastered the lower levels of the abstraction layer. You cannot study any subfield of systems programming without having understood the basic implementation of the underlying software. No amount of syntax rewriting is going to change that; those definitions are not going anywhere."

I don't see how that statement would make any sense. I expect to be able to give anyone with the most basic of understandings of computers a piece of any code (from Assembly to high level Lisp code) from widely used software like the Linux kernel all the way to stock trading applications and I expect them to understand it by looking at it for a few seconds, reading the comments, and reading the names of the variables and functions.

If the average person cannot do that, then it's bad code. Understand-ability is the only point of programming. To be understood by the computer and by a maintainer.

I'd never say that obtuse notations for an abstraction should stay around. I'd replace the obtuse notation with a better abstraction.

Mathematics also comes with comments, many papers essentially consists of one giant comment for the proof in the appendix. Granted, many variable names could be a bit less terse, but it's just easier to write "let f be an arbitrary function A -> B" once instead of using arbitraryFunctionMappingTheSetOf{DefinitionOfElementsOfA}toTheSetOf{DefinitionOfElementsOfB} every time.

Function and Map are different concepts that should not be described together.

In CS I'd just say

   B = map(some_function, A)

Not in this context. Assuming you are using `map` in the CS sense, B is what is called the "image" of some_function (over the domain A).

In math, a function is a mapping.

Consider the type of `some_function`. In C like notation, it would be `foo some_function(goo x)`. Which indicates that some_function takes an arguement of type `goo` and returns a value of type `foo`. In other words, some_function maps Goo to Foo (where Goo and Foo represent the set of all values of type goo and foo).

    for i in range(10):
        print(i)

    for (int i = 0; i < 10; i++) printf("%d\n", i);

On the other side of the spectrum you have this:

    map(print, range(10))

Otherwise, for people who learned functional programming from the start, it's much easier to understand.

Take a few lines of COBOL, compile it, and how much actual machine work does that represent? Lots. Very dense.

I can assure you the only parody I found was how simple it was compared to how big of a fuss is being made. The notation conveyed the concept of an onto function in exactly the right number of symbols. Every logic step was there, bared to the eye:

A mapping from [1...N] to [1...N] such that for every output, there is an input that maps to it.

As a sarcastic quip, what's so complicated about saying f[x]=y? (Equation wasn't the right word for you to use there).

> We dont expect CS people to communicate concepts through compiled, machine language style syntax

That is a complete misunderstanding of what this is. The symbols (and concepts) on this webpage are roughly equivalent to big-O notation in the Computer Science curriculum, in that they are taught in the first undergraduate course that tries to establish some theoretical basis for the subject.

IMO that line was the worst offender by far. Just use f(x), especially when you're giving an oral presentation to people who aren't familiar with the context in which the brackets are standards (TLA). Just because your formal system uses brackets for function application don't mean you need to obfuscate your slides.

"I had this talk where I wanted to feel superior so I showed an obtuse way to notate a simple situation"

"You can see my code I showed a room full of people who have more important things to do then to study arcane math symbols that are of no use to them:" https://github.com/EnterpriseQualityCoding/FizzBuzzEnterpris...

"I mean who in the hell could call themselves a mathematician without learning how to recognize obscure abstraction principles and language features of Java, something they'll probably never need to use?!?!"

"Some of these people where even smart, I tell you! They are big people who are productive but I have no idea how you could be productive or smart without knowing how to recognize this obscure thing"

Seriously, if you pulled in a bunch of CS people and showed them this:

    lambda x: x

Giving a legend explaining those symbols would turn the statement into this:

Given a function (f) that maps integers in the range 1 to n onto the same range (1 to n), for every y in that range (1 to n) there exists an x in that same range (1 to n) where applying the function (f) to an input x results in the value y.

(please correct the parts I got incorrect, it's been a while since my last discrete math class).

These symbols are important tools in discrete mathematics, but are easy to forget or get lost in due to the very high information density they achieve. Adding to the complexity, we explain the range of both inputs and outputs before defining the function. Intuitively, I feel CS folks would prefer to define the input range, the function's mode of operation, and finally the mapped output range.

This is especially complex when these discrete mathematics symbols operate upon one another. Throw in some sigmas and boolean operations, and it quickly become very difficult to parse.

The underlying intuition the author is trying to communicate is likely something that entire audience could understand. They simply weren't fluent in the "language" of mathematics. It's like being very articulate in English, and having to defend a thesis in French. Not only do you have to translate your thoughts, many idioms you may usually rely on are no longer valid in a new language.

Finally, why not define that same statement in Python or matlab? It's just as valid in my opinion.

Granted, my bachelor's isn't even a scientific degree, I'm an ex-addict turned sysadmin recently turned programmer, self-taught entirely. But I'm freaking sad I was a dumb kid who thought math was stupid once and that our school system (Germany) made it so easy to use my talent for language to average out my dare-I-say intentionally bad grades in the subject.

It's not even that I was bad at it. What drove me to computers, to code or crafting ridiculous zsh scripts in the first place was formulating my own approach to solving a problem. As much as I sucked at "solve these twenty equations like this", I used to love problems stated in natural language and coming up with a solution. Should've built on that.

Anyway, besides the late night regret... Can anyone of you recommend a book for me? Think little to no familiarity with the terminology, many years of only using what math a supermarket or insurance situation entails, eagerness to learn and fascination with the subject. No delusions about becoming a regular mathlete in my early thirties, I just want to fix a lack of knowledge caused by pubescent idiocy.

Thanks!

Not that I believe mathematicians should learn how to code as a perquisite for their degree, I don't. I also have similar feelings for CS students and understanding mathematical notation. Yes, if you're headed for grad school or a researcher, then it's a different story (so the grad students/academics should have tried may be). But should knowing that notation, say, be on the same level of importance for understanding programming concepts like cache-locality for someone headed to a typical dev job? Probably not.

How do you do any computer science without knowing the symbols for "for all" and "there exists"?

I think even when I was spending a lot of time on this in my CS degree that kind of notation gave me issues.

This is like giving an algorithms class to a mixed group of perl and Haskell programmers, using Haskell for all the examples and wondering why perl programmers don't learn computer science.

If you don't speak the language, It indicates that you never learned the stuff that is spoken in that language. At least well enough to be fluent in it.

Not true. I learned all the maths necessary to understand that formula and, in fact, have previously seen all the symbols used before. Once I looked up the syntax I had no trouble understanding what was being said.

The problem is that the language is simply bad. I haven't written PHP for years (in fact, the last time I wrote PHP was around the last time I took a math class), but if you give me a snippet of PHP I'll have no trouble understanding it.

Or more simply put, do you think these people have never taken a math class in high school that went over

    y = f(x)

If you study math enough, you learn to read this math notation fluently. From his toy example you can infer that they have not studied much math very deeply. Like topology or advanced algebra.

As another analogy, it's like an English speaking person taking a french basic-math class. You know like addition, subtraction, etc.. but taught in french.

The problem is that's it's been 12 years since I used a differential equation or any of my other 'hard' math. It's really frustrating that I used to be able to look at these equations and know what they meant and now I can barely make heads or tails of simple f(x) type stuff. I could solve (simple) differential equations without even jotting a note down, I honestly don't know if I could read one now.

It sucks.

The analogy would be more like studying both, writing a formal type system for a programming language, then practising mathematics for twelve years, and still understanding the type system.

I think more people struggle reading math than understanding the concepts.

Also note that he inundated the audience with a different formula popping in random places of his screen every 5 seconds for at least the previous 2 minutes, with constant more or less related babbling.

It sounds to me like a dishonest behaviour and conclusion. I must say I am neither a mathematician, nor a computer scientist, so I don't have a side to take, and I understand the formula, but I would not have raised my hand due to the fact there was only 5 seconds between the time the formula popped up about at the third of an already filled screen, and the request to raise one's hand. (And also because the one who raises his hand may end up cleaning the toilets. Beware.)

Try writing traditional equations with your keyboard. Try posting your answer online. Modern computer science breaks down these symbols into plain english.

All in all I think it's a matter of preference which is in turn related to each individual's experiences.

[0] https://www.emacswiki.org/emacs/PrettyLambda

I appreciate mathematics, but because I don't use this notation on a regular basis, I wouldn't have been confident enough to raise my hand.

Not quite. APL.

https://en.wikipedia.org/wiki/APL_(programming_language)

However, since Uni I have rarely needed to use the math notation, and so I am unable to understand it without "interpreting" it. Such notations have most relevance to understanding database schemas and other set theory type problems, however, generally speaking, in software development using such a notation is unneeded.

In summary, the reason computer scientists don't know math is not because they haven't been taught it, but rather that the notations are not very relevant, and therefore soon forgotten.

    x

I haven't finished watching the talk yet, but he seems to be arguing that programming languages aren't expressive enough for mathematical purposes. I suspect he's not counting all of the wordy scaffolding necessary to support those terse equations. Can it all be combined into a formal language that stands on its own? If so, might it look like a programming language?

INTERVIEWER: What kind of training or type of thought leads to the greatest productivity in the computer field?

LAMPSON: From mathematics, you learn logical reasoning. You also learn what it means to prove something, as well as how to handle abstract essentials. From an experimental science such as physics, or from the humanities, you learn how to make connections in the real world by applying these abstractions.

[0] http://research.microsoft.com/en-us/um/people/blampson/37a-P...

Who am I to argue with Leslie Lamport, but still I reject the premise. Computer scientists do learn math, regardless of whether they read Greek-letter math notation. Write a function with a for loop or array map, and you've used all the same math concepts as this example formula.

All the best math comes with pictures anyway. ;)

And that answer is: most do. The fields are very complementary.

Set theory? I personally don't have need for that right now. But I've been working my way through https://pomax.github.io/bezierinfo/ which the most complete resource to bezier curves I've seen, including closed-form solutions, analytical methods, and interactive demos.

I didn't formally study math after grade 11. A lot of Math anxiety is simply being too young to have enough Knowledge or neuroconnections.

I'm 40, and while I do not understand Roger Penrose's Books, they don't intimidate me like they would have At age 20.

TL;DR Comp Sci I took was all math so I don't get the title!

Conversely, my master's program pretty much assumed you were comfortable with set theory. CS103 is a freshman/sophomore level class at Stanford and is a prerequisite/foundational course for the master's degree. I was out for five years before returning for my master's. It is 100% true that programming skills are more useful in industry, and re-learning the mathematics was the hardest part of returning to school after being out for five years.

With that said, machine learning is eating the world, and it requires a very good understanding of the underlying mathematics.

When phrased that way the answer is more obviously. I've learned plenty of things I have let myself forget.

Math is boring. Cryptic math is... cryptic.

CS is interesting because it's about logical expression. You have an idea, now figure out the steps to make that become reality. Sure, some higher maths may be required along the way, but almost always as an ancillary task.

A.K.A. writing a proof. Isn't that what mathematicians do all day?

On the other hand, what percentage of physicists understand string theory? I do not know where that figure lies, whether a low number would be a problem, or whether it would be relevant to the computer science case. I do suspect that I would be better at computing if I understood category theory or TLA+ (I would at least be better able to evaluate their prospects for advancing the field), and I am not going to make any excuses for my ignorance.

The entire formula of

{f ∈ [1..N ⟶ 1..N] : ∀ y ∈ 1..N : ∃ x ∈ 1..N : f[x]=y}

could actually be written as

[1..N ⟶ 1..N]

Most CS people myself included will not trust their own senses when confronted with such a tautological statement and continue to search for meaning where there is non because it is so common to encounter cases in your everyday code where something that you thought was dead code has actually semantic meaning.

His natural language description is somewhat lacking in that aspect

> I had already explained that [1..N ⟶ 1..N] is the set of functions that map the set 1..N of integers from 1 through N into itself,

Because it's incredibly simple, and expresses concepts they should already be familiar with as they're both incredibly basic and plenty relevant to CS. The notion of "one-to-one" and "onto" functions is taught in high-school algebra!

> What does it mean if they don't?

It mostly means they've not been using this notation, which is a problem not because the notation is necessarily perfect (although I dispute those saying what's used here is particularly arcane - this is super basic stuff) but because there is a whole lot of relevant knowledge encoded that way (including plenty of CS papers!) and clearly they haven't been accessing it.

The training in mathematics, operations research, and mathematical modeling has been extremely helpful in the way I approach and solve computer science problems. It has helped with everything from smart SQL queries to developing scalable software and enterprise architecture for software.

Mind, set-builder notation is a horrible crock, since you wind up not being able to say "image covers the entire codomain" in plain language.

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.

You might reasonably say, "This is all the more reason to spend a lot of time thinking of a good name!" While everyone else actually doing math would say, "I need to get my work done, so let's just pick a name and get on with it." When math is done right, the concept in your head is concrete and ingrained enough that the particular word your using isn't that important.

That being said, having done math research and software engineering, mathematicians do spend about as much time as software engineers naming things. It's just easier for software engineers.

That is your opinion. I know quite a few people, both natives and otherwise, who'd heartily disagree with it. :)

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)

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.

Mathematical and sheet music are both organically grown. They're like C++ for math and music, but with about fifty times more cruft. Our forebears just kept adding on to and expanding purely crap syntax because getting people to change the existing way they do things is nigh impossible. Going on to hail this as "refined" is beyond me.

EDIT: Sometimes, in maths, different disciplines have conflicting syntax. Rather than fixing this, we just resorted to overloading (see i vs. i in maths and physics). If any programmer encountered that kind of thing in a computer language they would describe it as clearly evil.

EDIT: For a funny take on musical notes, see: https://youtu.be/-3WuQxnA7Hg

Mathematicians aren't dumb. There's some element of tradition (that's a small part of the reason why many mathematicians prefer chalkboards to whiteboards) but most of the reason we use the notation we use is because it's the best way anyone has ever found to express rigorous, technical, creative, abstract thought cleanly and efficiently. Mathematicians routinely do completely /new/ work which requires us to invent entirely new notation out of wholecloth on the spot. The techniques we use are suited to this need. When we find something that's better, we use it. There isn't anything better yet.

It's easy to design a better toy system. It's very, very hard to design a non-toy system that encapsulates all of the information in a full orchestral score and makes it readable for players of all instruments.

Just as finding a complete and consistent set of axioms for all mathematics is impossible, a universal syntax without namespaces sounds inefficient.

Surely you're not talking about modern tuning standards.

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.

My math profs emphasized juggling multiple layers of logical abstraction and omitting all unneeded explanations, while the CS guys wanted everything in excruciating detail and extremely formal language.

My current course is Programming Language Semantics. It's all relations, functions, states, predicates, induction, etc. Greek letters are used all over the place. The topic is interesting and I love implementing semantics in Prolog, but the mathematical notation is painful.

Totally! That's why Perl has taken over the field of software engineering, vanquishing all who came before it.

And for the handful of people who find Perl hard to read and understand: choose another career because brevity and standard notation are critical for understanding, and Perl has that in more abundance than any other language. The problem, as it were, is you.

As a perl cum python developer, no. It's that I had to spend time reverse engineering the code I wrote last week, because of the hundreds of obscure symbols I cleverly used to reduce thirty lines of clear code to five lines of compact code.

Python and Ruby both have to deal with references (though much more indirectly via the concept of mutable objects), as well as arguments coming in as parameter lists (and dicts).

"Because I could"

More specifically, in very short programs, the shortcut values were actually valuable, and the mental overhead for interpreting them in short subroutines or programs was minimal. The problem is that programs don't stay static, and that single time-saving shortcut becomes two, then four, then eight, then...

Soon, it's an absolute mess.

Even once I realized the cost, I had to follow the coding conventions of those who had come before, at the cost of increasing the cognitive overhead even further. A self-reinforcing loop.

> not pass by reference, unlike just about any other scripting language

As Smaug says, Python is pass by value. The trick is that the value is always a reference to an object, or more specifically “pass-by-object-reference” (“Object references are passed by value.").

This causes a few subtle behavioral inconsistencies, such as the dreaded `def a(b=[]):` bug.

One of the uses of the notation is to serve as a map for a more long-winded description, as you can lose your place in verbose explanations when they begin to get complicated.

More importantly, perhaps, is their use when you are applying formal manipulations to them. I think author's point is that many computer scientists apparently lack the background to follow or evaluate some of the important current developments in their field.

You can look at each permutation as a (unique, one-to-one and onto) function from the set [1,2,3,...N] to positions labeled also [1,2,3,...N]. For it to be a permutation, each position needs to contain a single value, and each value needs to be at one single location. Since the domain and range of the function have the same (finite) number of elements, either of these properties implies the other.

Given that each f is a function, mapping each member of its domain to one member of its range, and that for each member of the range, there is a member of the domain that the given function maps to it, and that the domain and range are the same size, then there can be no member of the domain not mapped to some member of the range, and each member of the domain must be mapped to a distinct member of the range (or else there would not be enough members of the domain to cover all the members of the range), so, with the domain and range being the same set, each of the given functions is a permutation of the domain, and collectively they must be all of them.

This is a verbose version of the argument for this being the set the author says it is. Arguably, it would be easier to read if I had used x for 'member of the domain', y for 'member of the range' and f for 'the given function'.

There are so many ways to write the same idea in less symbols.

It can be written with fewer symbols: `f: [N]->[N] s.t. x != y => f(x) != f(y)` is an equivalent formulation, for instance (since f from a finite set to itself is surjective iff it is bijective iff it is injective). The quantification is now implicit in the "implies" symbol. Not sure how standard `[n]` is to refer to {1,2,…,n}; it was used commonly in my undergrad courses.

Programmers have moved away from single letter variable names to make things understandable, but mathematics, even in CS has not.

I think many CS students have problem with mathematical notation because it can be both accurate and syntactically very sloppy and informal at the same time. It's human language and notation, it's not for computers.

Your comment is needlessly rude and you don't give any evidence to support your contention.

If his argument is offended, I apologize. I don't think it's possible.

You say this like mathematicians haven't been doing this for thousands of years.

Moreover, you do realize that computers were invented by mathematicians, right?

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)

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!

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.

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.

[1. https://www.amazon.com/Introduction-Theory-Computation-Micha...]

(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.)

I do wonder sometimes if we are too focused on computer languages, to the detriment of tools (see also Animat's comment.)

For that audience, why do you even need it? Just say "the set of all permutations of N elements" or "the symmetric group S_N" if you're nasty.