Have opened a ticket on github with a related feature request:
https://github.com/nim-lang/Nim/issues/7122
But also bringing it up on the forum for possible further discussion.
Anyhow, I'm a big "high integrity"-type fanboy. I don't program in Ada (yet), but I'm really enthusiastic about it.
Nim already seems to borrow many features from Ada (I think Araq's even mentioned this before, I think it was something like providing Ada, but being blamed for C's shortcomings).
Anyhow, I figure it's a really nice idea to scavenge some ideas off of Ada 2012. Partly to help bring that kind of set of secure (or more importantly, high integrity/reliability) practices more to the mainstream (also, some further distinguishing of Nim vs other more mainstream langs than Ada).
We probably won't ever get to the level of "SPARK"-type static analysis, but base Ada alone, is I think leagues ahead of just about every other lang.
(implied here, also ideas like making "contract programming" libs, like NimContracts, part of the stdlib, or having floating-point range types, etc), as well as being able to promote Nim as having a focus on security/high integrity.
Thoughts on this?
There is a major problem with NimContracts --- macros cannot be used on module level (no {.push: contractual.}). There is no way to run a macro on any routine a type is passed to or returned from (which is essential for auto-magical type invariants).
On the other hand, SPARK-type static analysis is not necessary. Rust is a good example here: there are many excellent lint libraries which provide a programmer with useful lints (for coding style, design, optimization etc) at compile time. The thing is Rust has a much more powerful macro system, being able to run arbitrary code on every type or routine declaration etc.