It kinda reminds me of the debate whether functional programming is suitable for beginners, despite being simpler than imperative, while imperative is more familiar.
I am opposed to familiarity argument (I think classical predicate logic and existential quantifier are being taught in early high school, maybe sooner, so they are more familiar than lambda calculus).
Based on my own programming and math experience, I wish I learnt about functional programming, LC, dependent types and CHI much sooner. I don't think it has to be complicated, I know some attempts (although a bit incomplete) to show this to beginners - To Mock a Mockingbird, Haskell Programming from First Principles.