See also https://github.com/mflatt/shplait, which is a language with (1) the HM type system and (2) the same syntax that Rhombus uses. The language itself is implemented in Rhombus.
To quote the above person: "tell me you haven't read the article without telling me".
You thought that supporting multiple "programming paradigms" is a nice thing, but it's the opposite for teaching beginning student. Experienced programmers want expressivity/customization/choices to do whatever they want. That's not what newbies need when they get stuck on an assignment.
It's exciting to think of "Deep" checking as a complement to optional checking. Use a mix of both in one code base to play their strengths. For example it'd be great to define a deep type checked module for parsing data. You get static errors and runtime validation too. But, also, use that module from an optionally type checked module, which doesn't add any extra runtime costs if some of your other code / dependencies are untyped.
As a programmable programming language, I think it would be a shame if someone wants to use mutation and it's not available. On the other hand, if you don't want to use it, then don't use it! If you are a language creator that doesn't want your client to use variable mutation, you can even choose to not provide the construct very easily (see the Beginning Student Language which does exactly this).
In DrRacket, when the cursor is on an identifier, you can hover over the big arrow at the top right corner of the definition window. A popup will appear showing basic usage of functions / macros without detailed explanation. However, you can click "read more..." which will open up the full documentation in a browser. Also, this documentation is installed locally and does not require the internet.
