of course. There will absolutely need to be a way to specify intent in certain cases or override the judgement of the checker. That may come in the form of external annotation, or possibly internal annotation, which in principle is achievable using the same technique as you see in the "unitful" demo, though that's not ideal.

as for zig being specified, well, it's pre 1.0, and the authors have I believe, specifically called out specification as being "the first priority after 1.0".