Regarding SICM, Sussman et al. point out that the traditional notation for differential calculus contains "type errors". In particular they point this out regarding the Euler-Lagrange equations. And they then make the point that their "functional" notation (based on Spivak Calculus on Manifolds) is free of these type errors.

Obviously Sussman has a special relationship to Scheme, but I am curious whether it would have been beneficial for the code implementation (scmutils) to have used a statically typed language.

Do you (formalsystem or anyone else) know whether the Julia implementation makes much use of typing? I don't know Julia but from a few seconds googling it sounds like it's also not statically typed. I do wonder whether something like Haskell wouldn't make most sense for reimplementing scmutils -- you'd be able to make a lot of the pedagogical issues clear at compile time, in the type language alone (disregarding the actual implementation of the functions in the term language).