There is an example I love when talking about compile-time checks and high-performance computing: Philipp Oppermann wrote a type-safe paging system for a kernel with only two traits. Let's first understand the problem and then try the solution.
When a program uses the memory on a computer, it must separate virtual memory from physical memory. This is because each program running in the OS will think that the whole address space is theirs. This means that in a 64-bit machine, each program will think it has 16 exbibytes (EiB) of memory, 264 bytes.
That is, of course, not the case for any computer in the world, so what the kernel does is to move memory out of RAM to the HDD/SSD, and put in RAM the required ...
