I do hope you're right with them figuring it out. It's a killer feature Ada and/or SPARK need. The alternative is basically separation logic. That isn't going mainstream or significant commercial haha. For me, I prefer both to adopt each others' strengths to increase diversity in batteries-included, safe/secure, systems space.
https://www.reddit.com/r/ada/comments/6avcy4/odds_of_ruststy...
I do hope you're right with them figuring it out. It's a killer feature Ada and/or SPARK need. The alternative is basically separation logic. That isn't going mainstream or significant commercial haha. For me, I prefer both to adopt each others' strengths to increase diversity in batteries-included, safe/secure, systems space.