This issue expands a question raised by @FalcoGer in #3 (comment)_
The question there, reworded, is this: say I write some library code and then annotate it as satisfying some profile. Now, does the local static analysis 100% prove that my library code actually satisfies all the requirements of said profile? What if some requirements are infeasible to statically analyze?
To me, this suggests that there are some requirements of a profile that both (a) are essential to that profile's guarantees, and (b) cannot yet be proved via static analysis.
If this is the case, it stands to reason that somehow or other, the library author must ensure the profile obeys these invalidatable aspects.
So, my questions I'm posing are:
- Is my reasoning correct, i.e. there are fundamental parts of profiles that cannot be analyzed and must therefore be handled by authors?
- How do we keep track of these requirements? Is there anything stronger than just guidelines?
This issue expands a question raised by @FalcoGer in #3 (comment)_
The question there, reworded, is this: say I write some library code and then annotate it as satisfying some profile. Now, does the local static analysis 100% prove that my library code actually satisfies all the requirements of said profile? What if some requirements are infeasible to statically analyze?
To me, this suggests that there are some requirements of a profile that both (a) are essential to that profile's guarantees, and (b) cannot yet be proved via static analysis.
If this is the case, it stands to reason that somehow or other, the library author must ensure the profile obeys these invalidatable aspects.
So, my questions I'm posing are: