I think there’s a good argument to be made along the lines that formalization might not only make it so that RSI is secure, but that if it becomes the case that sufficiently advanced AI will optimize itself to be more symbolic-like in order to execute faster (i.e. not have to simulate algorithms in-weight) that formal methods could aid in all three: security (no escape), interpretability (forced-symbolic), and inner alignment (sybolic parts constrained to have certain properties).
I think there’s a good argument to be made along the lines that formalization might not only make it so that RSI is secure, but that if it becomes the case that sufficiently advanced AI will optimize itself to be more symbolic-like in order to execute faster (i.e. not have to simulate algorithms in-weight) that formal methods could aid in all three: security (no escape), interpretability (forced-symbolic), and inner alignment (sybolic parts constrained to have certain properties).
Then you’d only need to solve outer alignment.