Interesting points. Because it's easy to do the type checking at compile time for function prototypes (though we haven't implemented it yet) we haven't felt under pressure to use the `func(void)` notation, which has always felt somewhat uncouth to me.
The verbosity of the annotations is the most jarring thing at the beginning. However, do you find any of them unclear? Because we're optimising for similarity to C before terseness.