Resolve/C++

I'm currently taking CSE 221 at Ohio State, and they're teaching us Resolve/C++, which has been described as "C++, but more anal." It's transformed into valid C++ by a few header files with loads of #defines, plus a "Foundation" that serves as a sort of standard library. The main focus of the language is the relationship between the client and implementation code. Basically, every function and procedure (the language distinguishes between the two) has a formal comment containing detailed mathematical syntax, describing the requirements and results of the operation. However, the compiler does not actually read the comments; they exist solely for the benefit of the client coder. Anyone else have experience with this "learning tool"? Apparently there are at least a few successful developers who swear by it. It seems to me like a decent idea in theory, but wouldn't it be better to teach developers to write good comments and documentation in English? Mathematical notation can get quite nasty, even for simple operations. At the very least, it seems odd to teach abstract object-oriented concepts in the first real CSE course. Perhaps algorithms/lower level concepts would be more useful as an introduction. Thoughts?