Short answer: nothing. (Even Bret Victor's work doesn't begin to touch it. http://worrydream.com/ Although he is well cool along other dimensions!)
For the flavor, imagine a type-safe LISP that one edits though something like Brad Templeton's Alice Pascal https://www.templetons.com/brad/alice.html or Emacs ParEdit https://www.emacswiki.org/emacs/ParEdit so that an incorrect program cannot be described in the system. (You can make a program that doesn't do what you intended, but whatever it does it will do so correctly.)
For the underlying technology, I would recommend reading up on Conal Elliott's "Compiling to categories" http://conal.net/papers/compiling-to-categories/ The connection won't be immediately clear. The connective is the Joy programming language:
The key is to see Joy (as opposed to, say, LISP) as the sort-of-AST that HOS is manipulating. If you restrict Joy to its type-safe subset and squint a little you have HOS. Then as a kind of bonus, Joy code turns out to be perfect for the "Compiling to categories" stuff (which is beyond HOS.)
