Yes, that has always been my feeling about SICM (their mechanics version). It was very helpful to me to see the Euler-Lagrange equations explained in the way th

Yes, that has always been my feeling about SICM (their mechanics version). It was very helpful to me to see the Euler-Lagrange equations explained in the way they did, i.e. using Spivak's notation for differential calculus, as well as lisp. But they even state in the introduction that the reason they are taking that approach is because the traditional Leibniz-ish notation is full of type errors, so as you say there seems to be a huge question about why they didn't tackle it with a language with a rich type system like Haskell or Idris. I know they did lots of clever things with schema some of which would be impossible to realize similarly in non-lisps, but still.