neel_k

Most likely it will do the opposite.

Losing a year of revenue will straight up kill a bunch of universities, just like it would kill most businesses. However, the following year there will still be the same number of 18 year olds who want to go to college as usual, and so surviving universities will grow much bigger.

Bigger universities will grow bigger administrative arms, which will further isolate the leadership from students and academic and enable even more extractive policies, both because increased social distance makes cruelty more thinkable, and because the loss of competition makes it harder for students and academics to find an alternative.

In other words, wiping out a bunch of businesses reduces competition, and less competitive markets are more monopolistic.

TeXmacs is a marvel, and for literally decades I've wondered why it hasn't seen broader adoption.

Both go and OCaml use LR parser generators, precisely because they make it easy to give excellent error messages.

Basically the key insight is that you can use the parsing automaton state to classify syntax errors, which makes it as easy as falling off a log to produce good messages. The paper originating this technique is Clinton Jeffery's TOPLAS 2003 paper “Generating LR Syntax Error Messages from Examples.” This is what go uses, and OCaml uses a more advanced version of this technique introduced by Francois Pottier in his CC 2016 paper "Reachability and Error Diagnosis in LR(1) Parsers".

Basic blocks with arguments is purely an alternate syntax for SSA.

From a teaching perspective, I like blocks-with-arguments a lot better, since it lets students reuse their intuitions about tail-calling functions. However, there's no difference in expressive power between it and the standard SSA representation.

In modern terms, you can identify sequences and automata: a sequence is a current state, plus a transition function giving you the next element of the sequence and the next state. However, if every function is tracked by a computable process, then the transition function must also tracked by a computable process, and so every infinite sequence must be generated by a computable process.

This identification is precisely what choice sequences are used to rule out. If a sequence is genuinely arbitrary, then you cannot describe it up front with a finite amount of data and a finite rule for updating that data. Instead, you have to imagine a mathematician adding a new axiom at each time step about the next element of a choice sequence, and requiring that any constructions they do works uniformly regardless of what axioms may be chosen in the future.

In this picture, the total amount of axiomatic data is actually going up over time, and this is actually important for the results Brouwer proved. In particular, without the axioms for choice sequences, you cannot derive the strong counterexamples, because you need classically-false axioms to prove classically-false theorems (like the continuity of all real-valued functions).

You are being a bit too quick to equate finitism and constructivism. Hilbert was a finitist, but not a constructivist, and Brouwer was a constructivist, but he was not a finitist.

Brouwer's analysis of the continuum depends heavily upon the notion of a "free choice sequence" (aka a lawless sequence). The idea is that a creating subject -- i.e., you or me -- is free to make an unbounded sequence of choices to produce a sequence. At any finite time, you can only have made a finite number of arbitrary choices, but if you wait long enough you can make any number of arbitrary choices. Because these choices are arbitrary, free choice sequences cannot be described as being generated by any finite rule.

This is a constructive process, if you imagine (for example) generating a lawless sequence by throwing dice or from the clicks of a Geiger counter. But it's not a finitist one, because there is no finite data from which a choice sequence can be computed. This let Brouwer retain the idea that a mathematician can only have considered a finite amount of information at any point, without having to make any identification of the real numbers with computable functions.

In terms of complexity, there's an interesting analogy between choice sequences and the question of whether randomization gives you extra power -- the Miller-Rabin primality test lends immense force to the intuition that RP is stronger than P, but we might be centuries from proving it.

Even if we set aside randomness, though, an ultra-finitist/complexity-aware-logic is something that basically every logician I've ever talked to has agreed should exist, except we basically don't know how to do it. It's something that pretty clearly demands more creative insight than technical grunt, and unfortunately imaginative leaps don't come on demand. :/

Brouwer was absolutely not a finitist! Indeed, he completely rejected the idea that you could use formal logic to bound what mathematics could talk about.

A better (but still not entirely accurate) description would be that Brouwer had an epistemic conception of mathematical truth: mathematicians become able to assert mathematical truths as they engage in the process of constructing mathematical objects. This is indeed a constructive process, but it isn't finitistic -- for Brouwer mathematical reasoning is open-ended rather than a closed set of rules.

So much like Goedel (who disagreed with Brouwer in many other respects), Brouwer was totally committed to the idea that mathematical statements actually mean things. And because they carry meaning, the mathematical process and the properties of the mathematical objects created by a mathematician take precedence over the rules of logic.

This is why Brouwer rejected classical logic -- not because of any finitistic reason, but because (for example) classical logic permits disassembling the continuum into its set of points. Since (for Brouwer) the point of a continuum is that it is continuous, it followed that any logical principles (such as classical logic plus set theory) that permitted you to break up the continuum were fallacious. This is why he spent a lot of time on his so called "strong counterexamples", such as his proof that intuitionistically all total functions on the reals are continuous.

Notice that the direction of reasoning here is exactly the opposite of what a finitist would accept: Brouwer used the properties of the continuum to justify various finitary logical rules, rather than the other way around. The continuum was real, and logic just a façon-de-parler.

I find this kind of thing really interesting because it illustrates that the pretheoretical idea of truth can be formalized in many different ways, and that the various formalizations are not all compatible with each other. We are used to informal ideas like space having many different mathematical realizations -- metric spaces, topological spaces, vector spaces, etc -- but it is a little disconcerting (and a lot fascinating) to realize that logic and truth exhibit the same plural nature.

I think lifetimes and lvalues are both reasonably straightforward to understand in terms of linear logic.

IMO, the main difficulty with adding monad-like abstractions to Rust actually lies elsewhere, in the fact that Rust doesn't really have function types -- or rather, it has too many of them. Roughly speaking, Rust does not have a function type constructor. Instead, every function you define in Rust gets its own special, unique type, which implements a function interface -- of which there are three, Fn, FnMut and FnOnce, to represent the different ownership states of the variables captured in a closure.

This means that monad-style interfaces involving higher-order functions and higher kinds will end up needing not just polymorphism over type constructors, but also constrained polymorphism over interfaces. This represents a much more substantial extension to Rust's type system than you might first expect.

The reason Rust does this is because if every definition gets its own type, then type inference can tell you very precisely which functions are called where, which makes inlining a lot more precise and effective. This is an important piece of how Rust turns (for example) iterator-heavy code into efficient loops -- there are actually many fewer indirect calls than it superficially looks like.

Personally, I think this was a design mistake, but it is also a choice that I would not revisit now. Once a system is in the wild, with users who depend on you, we are usually constrained to evolutionary development rather than radical redesigns.

It's actually super easy to achieve in general: literally (and I genuinely mean literally) tens of thousands of primary schools manage it.

You need (a) the members of the culture to have a shared ethos that sees the work as a noble pursuit and work towards, (b) enough money to ensure the system has enough slack that people can take the initiative to do things like help each other without everything falling apart, but (c) not so much money flowing around that the ethos gets overwhelmed by self-interest.

The trouble is that at a few million dollars money becomes a motive with a universal adapter, and enough people will let ethics slide to score that trust and shared values become unreliable. So it's nearly impossible to achieve in a VC-backed startup setting.

If you really want academic research about how the mixture of altruism and self-interest affects the balance of rule-making and individual initiative, then IMO the best thing to read is the economist Julian le Grand's 2003 book _Motivation, Agency and Public Policy: Of Knights and Knaves, Pawns and Queens_.

Actually, there is a critically bad interaction between the way that garbage collection algorithms work and the LRU heuristic for swap. Tracing garbage collection algorithms work by doing a graph traversal that traces all the live pointers starting from the "root set" (ie, pointers in registers and on the stack) to find all the live objects.

Now, note that (a) the root set are the hottest objects in memory, and (b) they are the ones that gc algorithms touch first. As a result, when you are doing a gc, the LRU (least-recently-used) heuristic for managing swap ends up putting all the hottest data in the program onto disk. This is pretty much the pessimal thing for the kernel to do, and can tank performance by triple-digit factors.

However, this is entirely fixable!

The gc and the kernel need to cooperate to figure out what is okay to push to disk or not. Matthew Hertz, Yi Feng and Emery Berger have a really nice PLDI 2005 paper, Garbage Collection without Paging, which shows how you can make gc performance hundreds of times better with just a little kernel assistance.

However, because kernel developers do not program in garbage collected languages (they program in C, because that's what the kernel is written in), they don't understand garbage collection and are hostile to kernel changes to support it. Emery Berger told me they tried and failed to get the Linux kernel to support their changes, and people who worked on .NET told me they had similar experiences with the Windows kernel team.

It's taking on a fair amount of risk to use a language that (a) encourages the use of concurrency but (b) is not memory-safe when you do so, especially when writing network-facing code.

Go uses multi-word primitive values, which means assignments are not atomic. Consequently, racing assignment statements can leave objects in weird states that violate type and gc invariants. For example, racing assignments to a value of interface type can give you an object with the wrong dictionary for its data.

The argument for not worrying about this is that this is an unlikely scenario. It's reasonable to think in probabilistic terms when clients are not trying to break the software (eg, in games or office software). However, attackers are not probabilistic: they actively search out vulnerabilities and push on them, so potential vulnerabilities turn into actual vulnerabilities in predictable fashion.

> The only difference is that for some reason they dive right into esoteric definitions like "monoids" and "magmas" and "monads" instead of the bedrock useful things from algebra like "groups", "rings", "fields", etc.

A remark: from a programming perspective, monoids are not esoteric, and are indeed more important than any of the intro abstract algebra structures. This is because free monoids are ordered lists, the most fundamental data structure in all of programming.

You can have a long and productive career as a C programmer knowing nothing but how to create and iterate over arrays! Monoids are so important that every single modern language (from C++ and Java all the way to Haskell and Scala) devotes a HUGE amount of language and standard library surface area to render data structures as sequences.

They are so important that even a language like Haskell is willing to accept utterly nonsensical semantics (hello, Traversable) to better support sequences.

I half-agree with you.

The agreement part is that the algebraic structures that naturally arise in my programming experience are indeed ultra-basic: monoids, lattices, semirings, partial orders, and so on. (When I need elementary linear algebra things are getting fancy!)

The disagreement arises from the fact that the right home for these basic concepts is often surprisingly exotic. For example, it's often the case that what you need is not a monoid in the category of sets, but in the category of sets and relations or partial orders and monotone functions.

Another example is when you want to represent syntax trees with scoped binding structure. Now a syntax tree is the dumbest possible algebraic structure (it's a free algebra with all generators and no relations), but when you have binding you need a free algebra in the category of presheaves over finite sets and injections.

The founding act of denotational semantics was Scott's model of the untyped lambda calculus, which is surely the paradigmatic dynamically typed language. Moreover, its creation led to an immense body of work on type theory, because there are two two distinct, but related, intuitions underpinning what a type is.

On the one hand, you can think of starting with some given notion of computation (the lambda-calculus, say, or x86 machine code), and then you can think of types as picking out particular subsets of the set of valid programs. (In jargon, this is "types as retracts".)

In this view, a type is a property of a program. On the one hand, you can say that only things which pass type-checking are programs, and things which don't type check are simply not well-formed programs. In this view, a type is a kind of grammaticality constraint.

If you don't have a model of the untyped lambda calculus, you can't speak formally about the first view, which is very limiting. This is because being able to shift between the views is important for thinking flexibly about different kinds of problems.

Of course, you can also try to combine these two views. A few years back, Noam Zeilberger and Paul-Andre Mellies wrote a gorgeous paper, "Functors are Type Refinement Systems", which lays out the principles of how these two views interact.

http://noamz.org/papers/funts.pdf

The "normal" physical systems we build (say houses and hydraulic systems) are mostly "continuous". This means small changes in the inputs generally result in small changes in the behaviour of the system. So, for example, if the screws on your kitchen cabinet doors are not tightened quite enough, the cabinet doors might wobble a little -- that is, a small change resulted in a small change.

On the other hand, systems based on digital logic are very "discontinuous". A small changes in an input can result in the system behaving vastly different. A single-bit error in a computer program can result in an if-then-else switching from the true branch to the false branch, and thereby running an entirely different piece of code. So your computer is a single bit flip away from fintech entrepreneurs using your entire bank account to rent AWS time to mine Bitcoin.

In general, we are drawn to discrete logic because it's easy to write programs to do different things based on different inputs. However, von Neumann was worried about this, because no machine works perfectly -- every computer runs with a certain probability of error, and computers run fast enough that even a low probability of error can compounds very quickly. And if a single small error can result in radically different results, how can you trust the result of a computer program?

In this note, written in 1947, he expressed the hope that if you could make computers behave continuously, you could not worry about small errors, because they would only have a small impact on the result.

However, a few years later von Neumann ALSO invented the alternative, modern way of handling these issues! In his 1956 paper _The Synthesis of Reliable Organisms from Unreliable Parts_, he proved that it was possible to use redundancy in a way to drive the error probability arbitrarily low, enough that you COULD trust the output of a computation.

It may be professional deformation speaking, but they seem to be using "applied category theory" in a coherent and natural sense: they mean the theory of monoidal categories, (a) viewed as a generalization of linear algebra, and (b) omitting logic and programming language semantics as applications.

Given the centrality of linear algebra to applied mathematics (even in places where you wouldn't first expect, like the theory of regular expressions and finite automata), this seems like a perfectly sensible coinage.

(Even though I must admit I get my back up at the omission of categorical proof theory, it's perfectly natural as a sales pitch -- type theorists don't need to be convinced of the utility of category theory!)

> That's what the author called "alt" and I don't understand why the author objects to it.

His "neutral pseudocode" is Go, which lacks good support for parameterized types. As a result there would be quite a bit of boilerplate code in doing things this way.

This is also why the author remarks "For trivial examples this works well, but for more complicated types with complex keys, it may require creating new types."

This post is a nice example of why it is important to eliminate friction from a a language if you want to get people to use a particular feature. However, the goal of removing friction interacts poorly with an observation Bjarne Stroustrup once made, that:

* For new features, people insist on LOUD explicit syntax.

* For established features, people want terse notation.

That is, when a feature is new to a programmer, they want it to be loud to remind them that something unexpected is happening, and once it is known to them they want it to disappear so they can focus on their problem -- and if it doesn't disappear, the solution using it will be so noisy they won't do it that way.

I expect the ultimate solution to this problem involves IDE design, rather than language design....

Semantically, returning a sum type like Result<T,E> absolutely is the same thing as exceptions (ie, it's the exception monad).

However, there's one very important language design difference between this and Java-styled checked exceptions: using sum type gives you effect polymorphism for free. This means you can write (say) a map function which says it has precisely the same exception type of its argument function, using the same machinery you're using for generics everywhere else.

This is a big from the usability side, since AFAICT it was the lack of effect polymorphism that turned people off of Java-style checked exceptions. From a language implementation standpoint, it's also nice not to have to implement type inference twice, once for return values and once for exceptions. :)

No. From an implementation POV, Prolog adds two pieces to ordinary programming languages: backtracking plus unification. This post talks about backtracking, but doesn't touch upon unification at all.

Eleven years on, this remains one of my favorite papers!

There's a pretty variant of this idea introduced in 1995 by Valentin Antimirov called partial derivatives of regular expressions. His idea was to replace the single derivative with a set of partial derivatives that add up to the whole derivative. This simplifies the derivative algorithm quite a bit, and makes it possible to write amazingly concise and efficient regular expression matchers.

E.g., here's an implementation of a regular expression compiler that uses Antimirov derivatives to take a regexp and build a table-driven matcher in about 50 lines of code:

http://semantic-domain.blogspot.com/2013/11/antimirov-deriva...

Hello,

You can see the current version of the class at:

https://www.cl.cam.ac.uk/teaching/1819/ProgC

I've moved to a style where the lectures are recorded and the lecture hours have been replaced with lab sessions. I've also mostly[1] removed the C++ content and replaced it with more C. Both the videos and the labs should be available for everybody.[2]

This gives more time for tooling (eg, ASan/MSan/UBSan/valgrind), as well as for various low-level topics like memory management (eg, arenas, reference counting and mark-and-sweep) and data-structure layout and cache optimizations (ie, the reasons why people still use C). Also there's a heavy focus on the lack of safety and undefined behaviour -- beyond the lecture devoted to it, this comes up in basically every lecture.

[1] There are still 2 lectures on C++. If you think that it is impossible to learn C++ in 2 one-hour lectures, you are correct. The pedagogical theory at work is basically "Dumbo's magic feather": the goal is to give students enough self-confidence that the year after they won't be afraid to consider doing a final year project using C++ (eg, modifying a web browser), which is the point at which they will _actually_ learn C++.

[2] I'm not totally sure how I feel about this. On the one hand, obviously I'm happy anyone can access these resources.

But on the other, it's really easy to say subtly not-quite-right things when lecturing. If it's ephemeral, then this is harmless since the effect of lectures is just to cue students too remember what to look up when they are programming on their own, but if they can re-watch the video then there's a bigger risk of burning in the wrong idea.

I suppose the long-term thing is to pre-write a script for each lecture, maybe even turn it into a book.

The literature on this subject is both vast and populated by the work of the most eminent philosophers -- both continental and analytic -- of the last two hundred years.

Here are some books that I liked. However, there are three caveats. First, being a great philosopher does not mean that one is a great writer. Second, I don't agree with all of these philosophers (indeed, most of them don't agree with _themselves_, since they changed their minds over time). Finally, I myself am not a philosopher, so this list is necessarily somewhat idiosyncratic:

- Edmund Husserl's Philosophy of Arithmetic and Logical Investigations. In the first, he studies what we mean by numbers, and comes to (in my view) a very modern cognitive-scientific/computer-scientific view (ie, that we have direct access only to very small numbers and that our understanding of bigger numbers is symbolic). In the second, he turns around and rejects the idea that reductionism can turn logic into psychology, inventing phenomenology in the process and authoring the root source of modern continental philosophy.

- Alain Badiou's _Number and Numbers_. If you need a Maoist continental philosopher who would disdain the entire Internet Bayesian rationalist community for being a bunch of squishy relativists who don't genuinely believe in capital-T Truth or capital-R Reality, then have I got the man for you! (After all, one should believe in true things because they are true, not because it would let you win a bloody bet. You should believe in true things even if that would make you lose a bet.)

Badiou is a hard-core set-theoretic Platonist realist who passionately hates everything in logic that I love ("[...] if it is true that mathematics, the highest expression of pure thought, in the final analysis consists of nothing but syntactical apparatuses, grammars of signs, then a fortiori all thought falls under the constitutive rule of language"), and I love him for it.

- Ludwig Wittgenstein's _Tractatus Logico-Philosophicus_and Philosophical Investigations_. I find PI much more convincing than the Tractatus, but it's worth reading because it makes a strongly-argued case for logical realism. The big danger with Wittgenstein is that his epigrammatic style is infectious (he's the best writer on this list by a country mile).

- David Lewis's books _Convention_ and _Counterfactuals_. I read _Convention_ as formalizing Wittgenstein's idea of a language-game in terms of game theoretic ideas of equilibria (as well as less formal ideas like Schelling points). _Counterfactuals_ is good (despite Lewis's bonkers modal realism) because counterfactuals and causation are an important part of actual real-world-applicable logic (as opposed to formal logic).

- Michael Dummett's On the Logical Basis of Metaphysics. This is probably the book that has had the biggest impact on how I think about everything. His analysis of realism anti-realism is beautiful and subtle, and makes one of the best arguments for intuitionistic mathematics I have ever read.

Grad students are actually more expensive, because they're slower and more likely to mess up than a pro would. However, you still want the grad students to do it.

A successful experimental physicist needs to have a deep feeling for how their experimental apparatuses work, including all the grungy real-world details that theoretical models don't cover.

You get that feeling by building and using the tools, and since the point of being a grad student is to learn how to be a successful experimental physicist, they've got to be the ones who build the tools!

Yes, the UK government is behind the erosion of free speech on campus.

The Counter Terrorism and Security Act of 2015 imposes a statutory duty on universities to have a "due regard to the need to prevent individuals from being drawn into terrorism". This means that institutions now have a statutory duty to participate in the government's Prevent strategy. This means UK universities have a legal obligation to narc on students who are too Muslim.

As a whole, universities have tried to finesse this attack on free expression this by defining violent radicalism as a signal of mental illness and telling us lecturers that we should feel obliged to refer struggling students to mental health services. Ultimately, though, when the intent and design of the rules is fundamentally bigoted, there is only so far that technical compliance can mitigate that.

Making parsing easily incrementalizable is a valuable property, because gramars which incrementalize easily also localize parse errors well, and having both of these properties hold lets you offer convenient APIs for IDEs and text editors much more easily.

For this, you want (as much as possible) for local edits to result in local modifications to the syntax tree, and ensuring that can require thinking carefully both about lexical syntax and abstract syntax. At the lexical level, if the literal syntax forbids newlines in string literals, then the changes to the token stream on a single-character edit are limited to changes to the tokens on the same line. Likewise, in the abstract syntax, if top-level declarations have a keyword, then the effect of a single-token change (eg, adding a mismatched paren) are limited to the declaration it occurs in.

There are a lot of tricks like this (eg, setting things up so you can find and parse the type declarations without having to parse a whole expression), but it's reasonable not to want to learn them. In that case, a really good heuristic is to make your language LL(1) parseable. It's not perfect, but it will rule out the vast majority of things that make incrementalization hard.

> Are models of observational type theory exactly elementary toposes?

By design, the answer is no. Toposes are models of intuitionistic bounded ZF. However, in general dependent type theories, including observational type theory, don't have (and don't want!) the powerset axiom.

There has been some recentish work on predicative analogues of toposes, but I'm not sure anything really definitive has emerged. However, I'm not super familiar with this area.

> To me, it still doesn't answer why TT is the most convenient axiomatization though. The internal language. [...] Especially because TT was arrived at from the IMO wrong angle, namely by coming up with a syntax first and its meaning second.

This is a very common misconception about what is going on when doing type theory.

From the point of view of a category theorist, the way to understand type theory is that it is a methodology for giving explicit presentations of free structures, in such a way that the morphisms make no explicit reference to composition.

The basic method of categorical logic is to compute a result in a syntax corresponding to a free structure, and then sending it to whichever non-free structure you like by the universal property of that structure. Most people initially find this a bizarre thing to do, since intuitively it seems like any proof that works in a free structure should work in any structure.

Indeed, this is actually true, if we only use the free gadget's universal property. However, if we have a type-theoretic presentation of a free structure, we actually have more information than the universal property: we know properties of the syntax! So we can exploit these properties of the syntax to establish facts which hold everywhere, by means of proofs that wouldn't work in an arbitrary structure.

For example, this is why type theorists devote so much effort on properties like cut-elimination: it ensures the composition of morphisms is automatically unital and associative.

Mike Shulman has written a fantastic set of notes, "Categorical Logic from a Categorical Point of View", which is one of the best explanation of type theory for "normal" mathematicians I've seen.

https://mikeshulman.github.io/catlog/catlog.pdf

Oh, wow -- thanks especially for that second link! I was wondering about this recently.

I should add that Gordon Plotkin gave a keynote at POPL this year, Some Principles of Differentiable Programming, where he discusses this from the angle of probabilistic programming. It's on Youtube at:

https://www.youtube.com/watch?v=qhPBfysSYI8

It's a really inspiring talk, albeit super intense (you need to be bilingual in denotational semantics and real analysis to follow everything).

At a super high level, the central problem is higher-order functions.

If you have a programming language, you can think of differentiation as being a higher-order function that takes a function a and returns a new function as a result. If your language has support for higher-order functions, then (a) you have to extend the definition of the derivative to cope with differentiation at higher type, and (b) ideally you'd like differentiation to be an operator in your programming language.

In general this is hard, so you have to cut the problem somewhere.

Pearlmutter and Siskind's basic idea is to use Reynolds defunctionalization transformation to turn higher-order programs into first-order programs, and then apply automatic differentiation to the resulting first-order program.

The approach in this talk is inspired by "differential lambda calculus", which is a setting where you retain full first-class functions, but restrict how you can use them by imposing certain typing constraints upon them (basically to ensure smoothness/differentiability of definable functions).

There is a mysterious connection between these ideas, since defunctionalization is closely related to the "geometry of interaction" semantics of linear logic, and differential lambda calculus is closely related to the vector space semantics of linear logic.

In addition to these semantic issues, there's also the question of how you hook it up to the actual algorithms people use to do gradient descent -- eg you need to use the Riesz representation theorem to justify representing the gradient as a matrix -- and that constrains how things could work even further. This is simultaneously annoying (because it makes things harder) and helpful (at higher type we have too much freedom in how to define the derivative, and so additional requirements help constrain the solution space).

So you might ask: why do we care so much about higher-order functions? The answer is that "higher-order function" is how semanticists pronounce "linking" and "separate compilation". It would be super great if we could take a bunch of teeny-tiny separately-developed models together, stick them together, and have everything work no problem.

> Also, does anyone know if what he refers to as "progress and preservation" are the same / related to "liveness and safety" in distributed algorithms? It sounds like the same kind of idea.

Progress and preservation are used to prove type safety, which (like the name says) is a safety property. Informally, safety means "a bad thing never happens", and liveness means "a good thing will eventually happen".

Informally, progress means "a typed program will never immediately exhibit undefined behaviour", and preservation means "a typed program always stays well-typed". Together, these two properties mean "a typed program never exhibits undefined behaviour".

This has the shape of a safety property. All this can be made much more formal, but that's the intuition.