> https://lamport.azurewebsites.net/pubs/hyper2.pdf https://lamport.azurewebsites.net/pubs/hyper2.pdf What the parent post talks about is not even close what i

> https://lamport.azurewebsites.net/pubs/hyper2.pdf https://lamport.azurewebsites.net/pubs/hyper2.pdf What the parent post talks about is not even close what is described in that PDF above. "Proving" (or better verifying) stuff at runtime is trivial as it's only some asserts at the end. Analyzing the properties of programs before you run them is in an entire different league OTOH.