Isn’t this a very restrictive way to write? Hard for me to imagine as never wrote with such annotations so no idea how viable it is for a large codebase to have this constraint.
Sure, but you want restrictions. You can't get an annotation that magically eliminates (de)allocation errors. It comes at a cost. The advantage of this particular proposal is its simplicity, I think. Otherwise, you'd have to get into contracts with complex expressions and then you'll have to prove those expression hold, and before you know it, your program is filled with proof statements. At least, that's my (limited) experience in SPARK, where you even can't have pointers.
Isn’t this a very restrictive way to write? Hard for me to imagine as never wrote with such annotations so no idea how viable it is for a large codebase to have this constraint.
Sure, but you want restrictions. You can't get an annotation that magically eliminates (de)allocation errors. It comes at a cost. The advantage of this particular proposal is its simplicity, I think. Otherwise, you'd have to get into contracts with complex expressions and then you'll have to prove those expression hold, and before you know it, your program is filled with proof statements. At least, that's my (limited) experience in SPARK, where you even can't have pointers.
My point is can you write a json deserializer with this, where allocation of every child is defacto optional, depending on input JSON?
1 reply →