I think iii is the most interesting of those. How to succinctly describe formal systems is a very hard topic. The kind of mathematical notation we use in classi

I think iii is the most interesting of those. How to succinctly describe formal systems is a very hard topic. The kind of mathematical notation we use in classical mathematics (algebra through calculus) is an amazing achievement developed over centuries (most of it since the 14th century!). But it only describes the existence of a calculation to be performed, not that actual method of calculation (the algorithm). Our ability to represent the methods of that calculation are extremely primitive. I suppose Lambda calculus is pretty close as are most modern programming languages. Upper and lower bound notation (like big-O) isn't bad as a kind of descriptor, but it's very restrictive in what you can do with it. I've seen certain kinds of state notation that's interesting-ish. But nothing approaches the elegance, flexibility (it's easy to abuse in good ways), extensibility, simplicity and efficiency of math notation (though even that system falls down when doing lots of matrix calculations by hand). But it beats the pants off of any other system I've seen for general mathematics. Most of the things that we deal with in CS are so big and complex that even diagramming them by hand would take longer than we'd want and require more paper than we have. In math we have some nice symbols to bundle all that complexity up, like pi, or summation, or limit notation. In CS we lack that. Most of the time we try and get by with toy examples, like graphs with half-a-dozen nodes, or small trees only a couple levels deep with different colored lines or some such -- most of it seems to be diagrams and tables...lots and lots and lots of diagrams and tables. Regular Expressions seemed about as close as we ever got to describing something succinctly. Learning how to manipulate graphs just off of the regexes was a very cool experience. I remember distinctly how frustrated my CS professors were compared to my Mathematics professors when trying to explain some concept on the board. I don't ever recall seeing a nice symbol that represented say, a tree, with some various super or subscripts that succinctly described all of the properties of that tree and the algorithm we were going to be using. Imagine how powerful it would be to write down, with just a few strokes, a short series of symbols that unambiguously defined a red-black tree and a search algorithm that runs in such and such min-time-complexity, max-time-complexity, and average-complexity as just a simple operator! Maybe something as simple as Y(rb) + s(log n, log n, "search term") = [s|earch term] or some such! But alas, I'm just falling back on a slightly bruised mathematic formal notation, not really anything new. Given how rudimentary the tools are we have to work with, it's amazing how far we've come in so short a time.