63 ms·

Nice summary. I've not been involved with formal methods for 15 years (at what is now Altran UK) so I'm rather rusty. Wasn't B an attempt at bridging the gap

• pron 7y ago
  I don't know B, and I think you are correct, but it, too, doesn't break the "scalability barrier". It would allow you to generate small programs by a process of refinement, but not very large ones. I think it is aimed mostly at safety-critical realtime embedded systems (and I believe it's used mostly for railways), so it's extremely useful (like other model-checked languages for that domain, like SCADE), but not something that can significantly help mainstream software.
  • noneeeed 7y ago
    Absolutely, none of the current formal methods approach scale to the level of much commercial software. Much of the systems engineering work that we did at Altran was focused on minimising the extent of the system that would need the higher levels of verification. So flow analysis and absence of runtime error proofs were commonplace, but proof of correctness against the spec was something that was much more focused on specific very high integrity components. I remember thinking that B was a heck of a lot of work for event the smallest projects. I'm kind of surprised that it's still being used.