91–100 of 232 posts
Back when I did my CS degree, we were taught the "B-method": https://en.wikipedia.org/wiki/B-Method The course dropped in popularity with students and the university eventually dropped it. Looking back on it, it really should've been a mandatory course for all software engineering students.
Formal methods will win when I can point the tools at a mess of C/C++/whatever code and have the tool figure out the rest with minimal overhead from me. Sure, sprinkling a few hints in my code would be fine, but trying to implement my design in a formal language spec and then... convert it to my chosen language, with the chance that I'll introduce bugs, seems like a waste of time.
The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. They can't even imagine the problem well enough to discuss it let alone specify it. A very large proportion of failed projects I've seen is due to this break down. The people who have the time and…
>> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification
That is the problem. The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project exists.
Earlier quoted context omitted.
Strong type systems with type inference are new(ish) for a guy as old as me :-D
Standard ML has existed for 35 years. Even if you started programming with Fortran, it's been around longer than half of your career.
Probably due to some alums of INRIA using their particular implementation for their own projects.
Earlier quoted context omitted.
Standard ML has existed for 35 years. Even if you started programming with Fortran, it's been around longer than half of your career.
Be honest, until 10y ago, ml type inference was invisible to 90% of the coders. Probably rejected willingly even ('where are my objects?')
The really simple answer to this question is: because at a high level of abstraction, it isn't useful. Most applications are being specified by people who don't understand in any detail what they want the application to do. They can't even imagine the problem well enough to discuss it let alone specify it. A very large proportion of failed projects I've seen is due to this break down. The people who have the time and…
Completely agree. This line sums it up: >> Before we prove our code is correct, we need to know what is “correct”. This means having some form of specification That is the problem. The people who come up with the spec don't fully know what is required. It's even worse than that actually; the requirements change constantly to account for changes in the technological and business environment within which the project ex…
I think this is a bit of an overstatement, because it implies an often unrealistic separation between writing specs and writing implementations. There may be several levels of each, and the middle levels may overlap.
For example, it may well be the case that the management on a project don't get heavily involved with the technical details and just specify "A needs to communicate with B" as part of the high level requirements. That doesn't mean the technical people responsible for implementing those requirement won't specify detailed protocols at a lower level and wouldn't benefit from formal methods to help ensure correct implementation.
This problem apparently even extends to the model-checking software itself, resulting in systems reported to be correct when then network message saying it is flawed was lost:
https://blog.acolyer.org/2017/05/29/an-empirical-study-on-th...
Formal verification might be worthwhile for its own sake, but for most projects you just need your own code to not be any more buggy than the rest of the technology stack you use, which you aren't going to re-create from scratch in a formally verified way because that's way too much work and the existing tools are just so useful and convenient and just an rpm/yum/git command away.
The low-hanging fruit right now is to eradicate undefined behavior at all levels of the software stacks we use. This is a daunting task, but I think we'll get there eventually. Once we've banished heap corruption, segfaults, race conditions, and similar problems to the point where developers say "hey, I remember those things used to happen in the bad old days but these days I couldn't cause them if I tried" and we can be sure that if we call a function with the same input it will return the same result every time consistently, then is the time to consider formally proving that the result returned is correct.
(That isn't to say that there aren't some domains now where formal methods are tremendously useful. Also, sometimes one can make a productivity case rather than a product quality case for at least using semi-formal methods; using a language with a strict type system can mean spending less time trying to resolve weird bugs.)
I love the concept of formal methods. As someone who pushes for more determinism in software(yay state machines), I have long dreamed of using them to prove correctness. And then I go look at the goofy, domain-specific language I'd have to learn, roll my eyes, and get back to doing 'real work'. Formal methods will win when I can point the tools at a mess of C/C++/whatever code and have the tool figure out the rest wi…
“... For instance, you are asked to create an online order system. To do that you need to think about all the possible states of the system, such as how it behaves when a customer places an order, what happens if it is not found on stock or if the customer decides to change or delete the chosen item. The number of such states could reach 100 or more.”
This is why so much software is broken. The author just admitted that he can’t be bothered figuring out how the system he’s about to build should actually work. That’s a deeply strange mindset to me.