This is not a simple problem to tackle. The coding example is essentially a human-implemented type system. I don’t generally prefer Joel’s solution because if you have isolated this as a frequent problem you might as well elevate your solution to it into the type system and get compiler support. But as you see with programming languages, and with the math example provided, people swap rigour for simplicity and speed. I don’t think we can trade one off for the other in any generalized fashion. That is, we see an error and we feel we’ve opted too much for simplicity. We see few errors and a lot of structure and we feel like we’ve overburdened ourselves. We kind of train ourselves on recent memory.
Interestingly it’s our basic satisficing around our poor memories that defines where we set our tradeoff. A good argument for AGI beating us is that it painlessly chooses more rigour.
This is not a simple problem to tackle. The coding example is essentially a human-implemented type system. I don’t generally prefer Joel’s solution because if you have isolated this as a frequent problem you might as well elevate your solution to it into the type system and get compiler support. But as you see with programming languages, and with the math example provided, people swap rigour for simplicity and speed. I don’t think we can trade one off for the other in any generalized fashion. That is, we see an error and we feel we’ve opted too much for simplicity. We see few errors and a lot of structure and we feel like we’ve overburdened ourselves. We kind of train ourselves on recent memory.
Interestingly it’s our basic satisficing around our poor memories that defines where we set our tradeoff. A good argument for AGI beating us is that it painlessly chooses more rigour.