The verbosity I felt in Frama-C contracts (when I tried back when) e.g. was around C's lack of 'parameter passing intent' specification (Ada has in, out, in out, not just by-value, by-ref, by-constant-ref-but-have-fun-with-the-value. People pass their structures as reference (struct thing *) and you have to ensure everywhere that that pointer isn't null. Same for over/underflow that isn't implicit in C. So lots of things needed to be required/checked explicitly instead of implicitly of with typing in SPARK. Cbmc has a similar thing where it has options to insert check if you ask it, checks that cbmc decides where to put, but are not defined in the language.
As for the rest, I checked again some recent Frama-C examples after your reply and verbosity is on par (similar quantifiers, loop invariants, etc.) and I don't see 'extremely verbose' in neither. Mostly I was focused on implicit versus explicit (in a 'boilerplate' sense).
As for the decline of Ada I see different things in my industry and a language and environment that keeps evolving and getting into more industries and making strides in very interesting domains. The DOD isn't the most interesting indicator of the liveness of a language, and I'm not sure what Ariane 5 brings here, except that when you reuse a binary component in a different setting without integration testing you get wild French fireworks?
As for the 'can't program a basic list in rust' I can only say that 99.9% of the time we're not rewriting a basic data structure, we reuse one from some standard library or a trusted component library, and I may have seen maybe one bug in those in my 15y or sw engineering, and countless ones in app or business logic, or serialization/deserialisation code... So yeah, if rust, spark or other hard ass static analysis tools makers are reading this, please keep making proof & verification tech modular. The more the tech advances the more spark we can have proved automatically without proof chops, the safer the world will be. But let me opt in the very hard stuff, please... Let me put the effort where it counts.
As for the rest, I checked again some recent Frama-C examples after your reply and verbosity is on par (similar quantifiers, loop invariants, etc.) and I don't see 'extremely verbose' in neither. Mostly I was focused on implicit versus explicit (in a 'boilerplate' sense).
As for the decline of Ada I see different things in my industry and a language and environment that keeps evolving and getting into more industries and making strides in very interesting domains. The DOD isn't the most interesting indicator of the liveness of a language, and I'm not sure what Ariane 5 brings here, except that when you reuse a binary component in a different setting without integration testing you get wild French fireworks?
As for the 'can't program a basic list in rust' I can only say that 99.9% of the time we're not rewriting a basic data structure, we reuse one from some standard library or a trusted component library, and I may have seen maybe one bug in those in my 15y or sw engineering, and countless ones in app or business logic, or serialization/deserialisation code... So yeah, if rust, spark or other hard ass static analysis tools makers are reading this, please keep making proof & verification tech modular. The more the tech advances the more spark we can have proved automatically without proof chops, the safer the world will be. But let me opt in the very hard stuff, please... Let me put the effort where it counts.