> Is drnim seen as a complement to nim compiler type checking, trying to > balance speed of compilation and type checks in the compiler, with for more > deep static analysis the developer would decide to delegate to drnim before > integration, for instance?
That pretty much nails it. > Where drnim will stand? drnim focusses on verification via Hoare Triples and focusses on: * Prove the absence of "array index out of bounds" bugs. * Prove the absence of overflows. Nim's effect `.tag` system can probably be replaced by something more powerful/useful too with this technology.
