3 ms·
Although good, hasn't this just shifted the burden up a level? With formal methods, we can get proven-ish correct implementation, now we need bug-free specific
by TickleSteve 10y ago
Although good, hasn't this just shifted the burden up a level?
With formal methods, we can get proven-ish correct implementation, now we need bug-free specifications.... this in itself will be the next challenge.
In the real world, specifications are very incomplete and fuzzy, partly because the business-level specifications are also fuzzy.
This will not be a panacea, its simply shifted the burden up to a (possibly more manageable) level.
- nickpsecurity 10y ago"With formal methods, we can get proven-ish correct implementation, now we need bug-free specifications.... this in itself will be the next challenge." That's much better. See, before you needed to (a) understand a vague specification, (b) get your concrete version of it right, and (c) implement that specification. Now, you just trust a precise specification. That it's precise, esp if in Z or something, let's you check it against the people giving you vague stuff too by asking them questions. Solves lots of problems. Altran/Praxis Correct-by-Construction provides an illustration of how that works: http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf At another extreme, some companies capture requirements in formal logic then just compile them to code with logic programming languages like Mercury: http://www.missioncriticalit.com/development.html http://www.missioncriticalit.com/development.html Note: Not sure how well the last one works but worth mentioning that it's at least possible to go from specs to code in some places.