Very common ask from projects that want efficient executable code as well.
It would be very expensive to have enough static analysis/verification to detect when it is safe to rewrite myMap := myMap[k := v] as an update to a mutable value, so in the short term the better option is to offer Dafny bindings for target language implementations of mutable values with the appropriate specifications. These SHOULD be the concurrency-safe versions by default to ensure the specifications actually hold, but we could offer alternative faster versions that are only safe for sequential code.
alex-chew
commented
1 year ago
Very common ask from projects that want efficient executable code as well.
It would be very expensive to have enough static analysis/verification to detect when it is safe to rewrite
myMap := myMap[k := v]as an update to a mutable value, so in the short term the better option is to offer Dafny bindings for target language implementations of mutable values with the appropriate specifications. These SHOULD be the concurrency-safe versions by default to ensure the specifications actually hold, but we could offer alternative faster versions that are only safe for sequential code.