That's fair; thanks for the feedback! I'll tone down the gallows humor on future comments; gotta keep in mind that tone of voice doesn't come across.
BTW a money brain would arise out of, e.g., a merchant caste in a static medieval society after many millennia. Much better than a monkey brain, and more capable of solving alignment!
Beren, have you heard of dependent types, which are used in Coq, Agda, and Lean? (I don't mean to be flippant; your parenthetical just gives the impression that you hadn't come across them, because they can easily enforce integer bounds, for instance.)
Thanks for the great back-and-forth! Did you guys see the first author's comment? What are the main updates you've had re this debate now that it's been a couple years?
(There was already a linkpost.)