Better array syntax

[rurban]

Wouldn't it be much easier to declare arrays like C++ refs, just with constant or variable length for automatic bounds checking, without manual where clause.

Like &a[2] or &a[len] as signature,and then you also won't need to deref it.

[aep]

it actually used to be like that some months ago. (the syntax was bad but basically same idea) something around:

https://github.com/aep/zz/blob/6e6aba7d4c4f201aba9cc820e7085128bef81120/examples/array/src/main.zz

it's actually very inflexible and doesn't allow return modelling. i.e. a function cannot havea contract that says "i will work on any array with size N and then return an array with size N+1"

now i understand that the pre/post expressions are very noisy, and i'll gladly consider any ideas that you might have for improving the syntax for the most common cases.

actually just realized the example is actually also a show case for how inflexible it is. see this ugly hack

    at is bound<dst>;

that's needed because without quantifiable logic there's no way for the prover to connect the dots between 'at' and 'len'. this is why zz is so powerful now.

syntax being a totally different problem tho. maybe your suggestion is to actually to auto-generate the where expressions from something a little nicer to read?

[aep]

feel free to repopen if you have more input