On Mon, Oct 8, 2012 at 2:21 PM, Felipe Magno de Almeida <felipe.m.almeida@gmail.com> wrote:
On Mon, Oct 8, 2012 at 4:40 PM, Lorenzo Caminiti <lorcaminiti@gmail.com> wrote:
On Mon, Oct 8, 2012 at 12:02 PM, Evgeny Panasyuk <evgeny.panasyuk@gmail.com> wrote:
Currently, I inclined to following approach: 1. Compiler MUST not do any checks on axioms besides syntactic. 2. User has ALL responsibility on verifying axioms. 3. Compiler has rights to exploit any knowledge which it gets from axioms, regardless of fact if type fulfil them or not.
IMO, this is a rather weak motivation to support axioms especially in the core language (just the syntax check of some code that could otherwise and almost equivalently be written using code comments) but it seems to be the only sensible thing to do with axioms.
Despite the weak motivation, I'm thinking to support axioms in Boost.Contract so to check them syntactically. Ultimately, if users don't want to use axioms, they can just not use them (and maybe document the concept semantics via code comments).
You find compiler optimization from axioms a weak motivation (3)? Why?
Because if the primary role of axioms is to state concept's semantics then I'd expect them to be used to enforce concept's semantics (with some type of compile-time checking) instead than using them for some optimization that BTW is going to be compiler-specific. You standardize axioms but how would you standardize the optimization that a compilers will generate based on them? If such optimization cannot be standardized (I don't think it can) and if that is the main reason for axioms, why are axioms standardized? On a separate note, within the context of supporting axioms within a concept library, obviously (3) doesn't apply at all (but this is a different point). In any case weak != 0 so IMO there's some value != 0 in axioms as "comments that document the concept's semantics and that are checked for syntax errors". Please note that all of this is just my personal opinion. Thanks, --Lorenzo