Have you read a lot of biology papers? Are they all about operating microscopes?
As has been pointed out to me several times by CS academics, I could stand taking a course in type theory. I have a good intuitive sense about it (likely from my math background), but have no idea how to prove something about it.
A CS courseload certainly doesn't (and certainly not in the required selection of courses) cover soundness of a language. Even my theory-focused classload only covered automata up to proofs of regularity etc. This is, sort of, step 0 in soundness-proving methodologies, but it's only step zero.
The whole reason we want to prove a type system sound is so we can prove certain things about the programs that use that type system.
We use type systems to help abstract patterns of data into logical constructs that can be reasoned about. They are logic systems with grammar that describes relationships between axioms and constructs.
Seriously, go read a textbook and then we can pick this discussion up. Wikipedia has a good overview.
We don’t call set theory and category theory “computer science” unless it’s about programming computers.
Much as how people who study computability are computer scientist, even though none of the asymptomatic improvements to matrix multiplication since 1990 are even remotely relevant to any kind of real-life program.
Typed lambda calculus was formalized before the first programmable computers, and it's relation to programming wasn't clarified for another 20+ years (and real type systems don't really start to appear in programming languages for another decade after that afaik).
With a sound type system, you can do things like compose a new type out of other types, and it will work consistently (not produce weird edge behaviors).
For example, C's `void` type introduces anomalous behavior. A function returning `void` is not composable, e.g.:
void foo();
void v = foo();
not sure what you mean by this, because there's no such thing as programming without computers. (actually, the first computers were invented before programmable computers were invented)
1. take two slices of bread,
2. apply peanut butter to one side of one slice,
3. apply jelly to one side of the other slice,
4. place the slices together with the coated sides touching, and
5. enjoy.
The answer is: it runs on dad, poorly :)
Or, you really don't think I can design a logical grammar to formally express the creation of a PB&J?
But there is computer science not applied to computers: Operations research for instance is basically a branch of CS: it is not about programming and it has applications in business, logistics, etc.
My computer science degree covered a lot of topics that didn't require a computer, for example relational algebra, discrete mathematics, and introductory formal logic. Of course, the practical usages of these are often best done through a computer and programming, but it's not a requirement.
In reality all computer science degrees I'm familiar with make an attempt to expose students to relevant programming languages, it's simply practical and students demand it, but the details of coding style, how to use git, or similar topics may not be relevant in a computer science degree. That stuff isn't so hard to learn if you have clear guidelines and they have some baseline amount of intelligence which is one thing a degree tries to validate.
A computer is a machine which runs programs (it computes). That's literally the practical and theoretical basis for computing. Instead of running the program in our heads, we have designed machines to do it for us.
We can calculate SHA256 with a paper and pencil. But we created machines (computers) to compute for us, according to the instructions we give them (the program, the algorithm).
Computer Science is the study of how we design algorithms to process data. We do computer science using grammars that allow us to describe abstract operations on data. We categorize the different types of algorithmic solutions to problems. We study the limits of efficiency and prove things about the various classes of algorithmic problems and their solutions. We generally work with discrete structures and type systems (like our beloved lambda calculus, origin of the Y combinator).
You can design algorithms without ever compiling a single piece of code just like you can add numbers without ever using a calculator. In computer science we talk about abstract syntax trees, higher order functions, context free and regular grammars, finite state automata, logic, and numbers. You can even get meta and modify your own algorithm’s data as part of the algorithm itself. All this happens independent of a particular instance of a physical machine.
Programming means “issue instructions to a given instance of a machine so that it behaves a certain way”. We take all our theory and apply it to an electrical device that has a physical processor and fixed memory. We program a microchip by writing chains of instructions to its memory. We measure performance in cycles per second. When programming we talk about machine instructions, loadable images, calling conventions, binary interfaces, program counter, alignment, and words.
TL;DR: just go read the Wikipedia page on Computer Science, it’s quite clear.
Geezer reaction:
https://en.wikipedia.org/wiki/Computer_(occupation)