I suspect what you consider a 'gray area', spec considers the whole point. What is the specification for this function? It has a signature and a return value an

I suspect what you consider a 'gray area', spec considers the whole point. What is the specification for this function? It has a signature and a return value and some behaviour in between. Spec verifies all of that together because it doesn't make sense to do it separately. Also I'm not sure what you mean about run-time, you can and should use spec as part of your development workflow. Other two points are totally fair though, and the macros are part of the reason it never got out of alpha before a rewrite.