I find it interesting that goto is in the examples. I'm not deeply familiar with program theory and computability, but I thought goto made the program impossible both to reason about and to verify its correctness. Why would one include it in a new programming language? Are there really valid uses of it? I don't think the factorial example here is a good use - he basically used it as a while(true) infinite loop. However, I also couldn't tell you with accuracy why it might be bad here other than the ingrained mentality of goto=evil.