On Two Views of Computation in Computer Science

First, I don't think that the only way to assign meaning to computation is by formally assigning meaning to the syntactic components that comprise its program, as written in some human-readable language. Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators. Components' meaning may be stated informally. I am not aware that formal meaning is the only valid meaning. People wrote the software that landed men on the moon in assembly; that was pretty meaningful. I believe this is still the prevailing view in computer science.

Second, you keep identifying the notion of computation with the notion of a program written by a person. The theory of computation, from its earliest days -- by Turing himself -- has studied computational phenomena in neural networks, genetics (Turing was a pioneer of both NNs and genetic algorithms) and quantum phenomena. Some of the greatest achievements in CS are not specifically related to software (I count at least 20% of all Turing awards).

> For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning.

Or TLA+, which makes types notoriously more difficult to use by comparison.

AFAIK, the only languages that fully express the computational meaning formally with types are the dependently typed ones. AFAIK, there has been exactly one non-trivial real-world program written in such a language, and its author wasn't too pleased with the process (I'm referring to CompCert and Xavier Leroy). Every other program in every other languages has most of its meaning expressed informally, in the mind of the programmer. Unless you believe that no programs work, then nearly all programs that do express most of their meaning informally.

> Too much nonsense has been said as a result of not formalizing things.

Formalizing things doesn't imbue them with good sense. You can state plenty of nonsense formally. The only thing you're guaranteed is that it's consistent nonsense, and, as someone said on one of my favorite TV shows, "The sole virtue of the ineffectual is consistency".

> Which tool satisfies the following criteria? ...

TLA+, and far more elegantly and simply than any typed language you've seen.

> TLA+, and far more elegantly and simply than any typed language you've seen.

Still eagerly awaiting your elegant and simple explanation of this! It sounds groundbreaking (genuinely).

The inhabitants of the type `forall a. a -> a` (which, by the way, in an effectful, Turing-complete language, has more inhabitants than just the identity function) aren't in one-to-one correspondence with the inhabitants of the type `nat -> nat`. I asked for an isomorphism of types, you have to give me an isomorphism of types. Or maybe you don't know what “isomorphism” means in mathematics?

>> What category are you working on?

> I have no idea what point you're trying to make

Okay, you don't know what “isomorphism” means in mathematics.

> You're still wrong if you think the CTT is "true, but false if applied to matrix functions.

The CTT isn't “false if applied to matrix functions”. The CTT says nothing about functions at a type not isomorphic to `nat -> nat`. It would be like saying “SilasX is all wrong about frogs!”, when you never said anything about frogs (at least, in this discussion).

> No way could a computer handle that. They only know binaries numbers, not the matrix type. I mean, come on, I gave them a different name and everything!"

I write my programs in high-level programming languages, not machine language, though. The whole point to high-level programming languages is to reason in terms of their abstractions, not their possible implementations.

https://www.microsoft.com/en-us/research/wp-content/uploads/...

and an older paper covering an interesting theoretical property has over 1000. Also, the author did get a Turing award -- not primarily for this, but it got a mention. So yeah, we're talking about a very well-known formalism in software verification, and people were impressed. I don't know about groundbreaking because the community is different. In software verification you get points for new proof methods and such; not necessarily for creating an elegant language. TLA+ is about finding the ideas that have been shown to work at scale, and creating a very elegant, minimalist language to express them, based on simple ordinary math as much as possible.

There is no shortage of good tutorials (especially considering how simple TLA+ so there's no need for 500 tutorials on monads), and the language was designed for and is used by engineers in industry working on large, complex systems. Companies that have started to use TLA+ (or use it extensively) on large systems -- Amazon, Oracle and Microsoft -- report that their engineers pick it up on their own from available materials in two weeks (that was my experience, too; it's easier than most programming languages). But those are tutorials and don't focus on the theory. Amazon published two excellent technical reports, one in CACM, about their experience, with pretty good data (that's what convinced me; I'm impressed with what's been shown to work in the field).

There is also no lack in more academic, theoretical material, but, as usual, that is mostly concerned technical details.

What's missing is a brief overview of the theory. I'd read at least the introduction to the original paper above, this 4-page historical note[1], and this[2].

[1]: http://research.microsoft.com/en-us/um/people/lamport/pubs/c...

[2]: http://research.microsoft.com/en-us/um/people/lamport/pubs/s...