Rust and the price of ignoring theory

Description

00:00 Intro 00:50 What rust does 02:59 Memory management principles 05:30 Stack memory 08:04 Heap memory 09:07 Arenas 11:05 Maths vs Silicon 13:04 Garbage collectors 13:55 Example of Rust borrowing and lifetime subtyping 17:10 Safe in bounds access via dependent type. 18:37 Theory 19:45 Granule: Linearity 21:15 Linearity limitations 22:39 Ownership 25:27 Dark side of theory and of pragmatism 26:55 Dynamic linking 30:10 Security nightmare 35:47 Rust Miscellaneous advantages 40:06 Rust Rewrites: Discord (from Go), ripgrep (from C), rust (from Ocaml) 40:57 Ocaml modules 42:25 Compilation speed 43:34 Runtime speed 44:35 Linux kernel 45:25 GPU programming 45:52 Personal practice 49:18 Conclusion 51:52 Future Memory is the sort of barely relevant low-level detail that defies automation and obfuscates algorithms for no profit. At the same time, considerable performance can be won or lost and horrific bugs are at risk. Attempts to improve memory management are very welcome, but not if they repeat well understood mistakes of the past. Rust took one step forwards, and two steps backwards. There is something uniquely irritating about it's zealous and misleading marketing, wasted potential and gleeful disregard for the accumulated genius of decades of research. For all its obsession with security, rust's packaging and linking system end up creating more insecurity than it's limited model of safe memory can eliminate. -- References Functional Ownership through Fractional Uniqueness https://dl.acm.org/doi/10.1145/3649848 A Mixed Linear and Graded Logic: Proofs, Terms, and Models https://arxiv.org/abs/2401.17199 Granule github https://github.com/granule-project/granule Why not bundle dependencies https://wiki.gentoo.org/wiki/Why_not_bundle_dependencies