I don't see any meaningful distinction between human reasoning and logic, tbqh.
As I stated earlier, your stacks of scoped continuations are exactly equivalent to monads but, depending on how you restrict them, a little less flexible. I don't mean this to say something trivial—I mean it to say that every composition problem solved in each place is identically solved in the other.
I'm confident that your 99% claim holds historically to various degrees, but not completely. Plenty of mathematical algorithms were (a) constructive and (b) first formulated declaratively. We have spent the last 30-50 years describing many more algorithms at a much more furious pace at a time where publicity depended deeply upon using an imperative language... so historical explanations have that going for them.
> As I stated earlier, your stacks of scoped continuations are exactly equivalent to monads but, depending on how you restrict them, a little less flexible.
But they compose better, not requiring monad transformers while still being type-safe. For the continuation to decide on which scope to pause on is like a monadic function returning a monadic value of a monad not directly enclosing it, but one or more levels up.
As I stated earlier, your stacks of scoped continuations are exactly equivalent to monads but, depending on how you restrict them, a little less flexible. I don't mean this to say something trivial—I mean it to say that every composition problem solved in each place is identically solved in the other.
I'm confident that your 99% claim holds historically to various degrees, but not completely. Plenty of mathematical algorithms were (a) constructive and (b) first formulated declaratively. We have spent the last 30-50 years describing many more algorithms at a much more furious pace at a time where publicity depended deeply upon using an imperative language... so historical explanations have that going for them.