> > Yes writing the definitions by hand can time consuming and error-prone

> With the proper environment, this isn't that time consuming or error-prone anymore, based on my recent experiments.

If you have modules with automatic, and manual IMPLICIT and EXPLICIT tagging and you fail to translate those things correctly then you can trivially make mistakes that cause your implementation to not interoperate.