3 ms·

Not even going to dependent types, the type system and verification capabilities of the SPARK language & toolset already allow for use in the mission-critical (

Not even going to dependent types, the type system and verification capabilities of the SPARK language & toolset already allow for use in the mission-critical (and not only safety-critical) domain. The tech is progressive so you can go first for 'correct' data flow (no access to uninitialized variables, dataflow constraints like Depends, Global, very interesting stuff already), then for proof of the absence of runtime errors, then for some specific properties (think maybe properties like 'this should never happen' or properties you'd write when doing PBT) to full functional proof. On a procedure to procedure base. The progress that's been made with support of floating point is amazing. Things that were hard 3 years ago now get proved without help. Pointers are now supported via a rust-like mechanism. NVidia seems to believe in the tech (well at least for Ada) for some of its new firmwares. I've seen pure algorithmic code fully proven with similar effort as it would have taken testing /AND/ you always find bugs... People that have written some SPARK then start thinking and designing for proof. Code gets simpler, design clearer, loops more evident, added contracts help understanding the interface and clear the mind while reading code (like early returns would have done before). I don't work for AdaCore or Altran UK but I think they're amazing minds at work here.

pcwalton 7y ago
Maybe some folks are experimenting with it, but I would be shocked if SPARK achieves market share of 1%. Or 0.1%.
- touisteur 7y ago
  I think it's a bootstrapping problem, similar to rust adoption. People are now getting enthusiastic about a language with lots of static guarantees and a difficult-to-please compiler, and I keep reading people almost jumping to formal proof/verification ('now that I made all this effort and I get all those static guarantees, why not go the extra static verification mile ?'. I think the rust formal-methods community should look at what's already been done with Spark2014 (Ada) and Frama-C. A large part is an adaptation of the language for proof (adding /executable/ contracts, some quantifiers, loop variants/invariants, expression functions), and another big part of the work is in why3 and all the SMT tech behind, so can be re-used 'for free'. Sure not even 0.1% market share today, and I'm not even sure Ada is above this. But it's there, it's already mature, progress is very fast, and it can be tried out for free without 'asking for a quote'. Same for Frama-C. Sure it's a paradigm shift, but it's not an academic tool with an obscure UI and no retargetable skills.

pcwalton 7y ago

Maybe some folks are experimenting with it, but I would be shocked if SPARK achieves market share of 1%. Or 0.1%.

touisteur 7y ago
I think it's a bootstrapping problem, similar to rust adoption. People are now getting enthusiastic about a language with lots of static guarantees and a difficult-to-please compiler, and I keep reading people almost jumping to formal proof/verification ('now that I made all this effort and I get all those static guarantees, why not go the extra static verification mile ?'. I think the rust formal-methods community should look at what's already been done with Spark2014 (Ada) and Frama-C. A large part is an adaptation of the language for proof (adding /executable/ contracts, some quantifiers, loop variants/invariants, expression functions), and another big part of the work is in why3 and all the SMT tech behind, so can be re-used 'for free'. Sure not even 0.1% market share today, and I'm not even sure Ada is above this. But it's there, it's already mature, progress is very fast, and it can be tried out for free without 'asking for a quote'. Same for Frama-C. Sure it's a paradigm shift, but it's not an academic tool with an obscure UI and no retargetable skills.