By this, are you referring to annotations ala JavaScript @decorators or PHP #[attributes]? If so, I definitely see the value, as they make it easy to add functionality and static analysis information, but that very magic seems to be antithetical to Zig’s desire to be fiercely simple and avoid magic / hidden logic.
Thoughts?
Very much unlike JS and Python decorators, and fairly unlike PHP attributes as well.
The most important fact about annotations, and zig validate, would need to be that as far as the compiler is concerned, they’re just comments using a distinct syntax.
They would exist to further restrict the properties of a compile-able program, not to change the behavior of that program in any way.
Much like tests: a test suite provides validation of properties of a program which the compiler will happily let you violate.
An example of something worth annotating: “variable a_idx can only index slice_a, slice_a can only be indexed with a_idx”, which is logically two assertions.
The compiler has no problem with indexing slice_a with idx_b, as long as it’s an unsigned integer smaller than usize. Nor should it. That’s a program invariant, not an illegal operation.
But the validation step would fail if that invariant was violated. It isn’t practical to test this invariant, because it’s a property of the source code which isn’t visible from outside of the function. Hence the desire for a built-in extensible validation step.
What does validation code actually look like?
If this was implemented proceduraly, using something like operator overloading, then I would expect these assertions to happen at runtime (the compiler inserting checks on the type id of the index). This of course has the downside that its not happening at comptime.
If this was implemented declaratively, then we have the same problem with all declarative languages: they are limiting when people want procedures! Just look at how if statements are implemented in github actions, or godforsaken ansible yaml.
Do you think that the scope of validation is finite and small? If so, declarative could be ok, but I’m not sure anything could be made extensible enough to fit your use case.
For example, what if I want:
“slice_a can never be larger than 256 elements”. A lot of these problems are undecidable, i.e. “halting problems”, or np hard, whatever you want to call it. Problems that are impossible to prove.
I think this example is not a good one, because you can simply use assert in this case.
As a counter argument to this, if something requires this level of an assertion, would not a non-exhaustive enum provide the same benefit without needing to add a validation step to the compiler.
If you need to be sure that x is only ever accessed with y, this seems like the need for a custom data type and index. Admittedly, this complicates the code a bit compared to using a normal slice and index, but that seems like an acceptable tradeoff when you need this type of assertion.
It would receive the AST with attached annotations, and be able to call the compiler to create test programs if necessary. The last part is optional but probably good to have. The important part is that the compiler ignores validation, the way it ignores unit tests and comments, and that validation receive the source in a form amenable to static analysis. Whether it’s able to do runtime analysis as well is not central to the idea.
The answer to “procedurally or declaratively” is: neither of those things, or perhaps both. An annotation is declarative in essence, and the validator which does things with the annotation is fundamentally procedural. In principle the latter could be declarative, but I would anticipate validators being written in Zig, which is not a declarative programming language. Perhaps not entirely! But normally at least.
I don’t think that, but nor do I think the conclusion follows from the premise. The set of annotations, and the set of validators, would be open-ended. Presumably the validation code needed for the annotations actually in the program could be specified in build.zig.zon, and provided to the validate step using the normal mechanism in build.zig.
Some subset of annotation / validation pairs could be made a ‘depends on’ for building modules / executables / any other artifact, such that they would always run in that build step. That’s just a natural extension of how build.zig works, but by default validate would be a distinct step, as test is now.
Whether the Zig compiler ships with a set of validators, and whether some subset (perhaps the set itself) of those validators is standardized in the language definition, is an open question. I would say that with the door opened by providing annotations, it would make sense to include some validations, but it isn’t necessary. The specification of the compiler proper would only need to correctly parse annotation syntax, the way it will need to correctly parse comments. Specifying that anything beyond that is mandatory for a compliant Zig compiler is completely optional.
An example of a validation which has been proposed as special syntax is #21879. What I’m suggesting is close to the ‘linter’ variation, but linting, while related to validation, is not really the same concept (I also explicitly spell out this same idea later in the issue).
So the “useall validation” is a good example of one that Andrew thinks is worth adding to the language, and can serve as a reference type for the idea that the Zig compiler might include some set of validations to-be-determined.
An annotation must be matched with validation code in order to be useful. Your example is a good one, because there are in fact programs where this can be proven, and the advanced forms of validation are in fact theorem provers.
So a general system would allow (namespaced) annotations of any sort, but if your code makes a claim which no validator can prove, that’s a problem. If there’s no validation action included for the annotation once the namespace is resolved, that’s just a bug, if there is such a validation and it cannot prove the claim, that’s a failure to validate.
This doesn’t actually work. An index operation has to be coercible to usize or it fails the typecheck. So the index operation would have to use @intFromEnum, which doesn’t specify the type of the enum being cast, it works on any enum.
Some related problems can be solved using enum-newtype, this one cannot. It might lead to cleaner code to solve some of those problems with annotations and static analysis, or, it might not.
But there are clearly problems in static analysis which are beyond creative use of the existing methods we have, useall being another good example.