Something this misses is that all programs make assumptions for example - “my process is the only one writing this file because it created it” Evaluating corre

Something this misses is that all programs make assumptions for example - “my process is the only one writing this file because it created it” Evaluating correctness without that consideration is too high of a bar. Safety and correctness cannot be “impossible to misuse”