Toot

Written by Simon Tatham on 2025-01-10 at 09:57

@OscarCunningham I think one could probably make the isomorphic joke in programming languages, with 'safe by default' languages on the HoTT side (both Rust, and the larger and more established GC family) and 'close to the metal' languages on the ZFC side (most famously C and C++ these days, but also many other older languages).

In programming, there are two reasons for the unsafe languages to exist.

1. They're easier to invent and implement, so they came first; safe languages came along later.

2. They're a necessary substrate for implementing the safe languages. E.g. the (usual) Python interpreter is written in C, and the standard library used by safe Rust code has unsafe Rust inside it.

I guess HoTT is indeed newer than ZFC, paralleling reason 1. But reason 2 seems to have no analogue here.

=> More informations about this toot | View the thread | More toots from simontatham@hachyderm.io

Mentions

=> View OscarCunningham@mathstodon.xyz profile

Tags