formalizing the QACI alignment formal-goal — LessWrong