SPARK contracts look super interesting. It seems like that could let an optimizer do some great stuff and decrease the mental burden of reasoning about mostly p

SPARK contracts look super interesting. It seems like that could let an optimizer do some great stuff and decrease the mental burden of reasoning about mostly pure functions by calling out specific side effects. What is different about its types? I don't see anything obvious. What I'd miss about rust is the borrowchecker and const by default.