Regarding SICM, Sussman et al. point out that the traditional notation for differential calculus contains "type errors". In particular they point this out regar

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).