4 ms·
It doesn’t have to be that slow! The tooling has advanced quite significantly over the last few years.
by exdsq 7y ago
It doesn’t have to be that slow! The tooling has advanced quite significantly over the last few years.
- MaxBarraclough 7y agoIt's still fair to say that formal methods produces software far, far more slowly than ordinary methods. Look at how little functionality seL4 provides, compared to hobbyist operating systems.
- lmm 7y agoFor equal time and effort, I'm not at all convinced that it's slower. It's easy to underestimate how much time gets spent on debugging, you just don't see it in the up-front cost.
- thanksforfish 7y agoIf you don't use formal methods, how do you know when your work is done?
- im3w1l 7y agoWhen the checks clear.
- ternaryoperator 7y agoOne of the finest puns I've seen on HN ever!
- bluGill 7y agoWhen the rate of bugs coming in from test goes below some threshold that your boss is comfortable with. Note that formal methods don't get around this as they do nothing for the class of bugs where it works as specified but now that we see it in operation we know the specification was wrong. (once the spec is right though it is faster)
- deleted 7y ago[deleted]
- oldgradstudent 7y agoIf you do use formal methods, how do you know you completed the proof?
- MaxBarraclough 7y agoI don't follow. The proof is complete when all proof obligations have been discharged.
- oldgradstudent 7y agoBut how do you know you have the right proof obligations? It's very easy to discharge a massive number of proof obligations while proving nothing of interest. Formal methods don't just make bugs and debugging disappear, they just move it to a different domain - the development of the proofs.
- MaxBarraclough 7y agoI can't make sense of what you're saying. You've completed the proofs when you've discharged all proof obligations. The proof obligations will depend on the formal modelling system you use (Event-B, say), and of course on your formal model. You aren't left in a state of uncertainty as to whether you've finished discharging the proof obligations. Are you referring to the possibility of errors in your model? That's not the same thing.
- oldgradstudent 7y ago> Are you referring to the possibility of errors in your model? That's not the same thing. It is very easy to complete a proof on the wrong model, and there are always errors in the model, at least initially. There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough? That's quite similar to asking "If you don't use formal methods, how do you know when your work is done?"
- 7y ago
- ashafer 7y agoAs one of my coworkers put it: "A talented programmer can write and verify 4 lines of code a day" seL4 has some cool ideas, but I can't stress enough how miserable it is to develop for.
- CalChris 7y agoDo you mean it's miserable to develop the seL4 microkernel or do you mean it's miserable to develop applications on top of seL4? If the latter, is it any different from any other microkernel?
- exdsq 7y agoYou don't have to jump in 100%, you can just add formal methods to the things that require it. Cryptographic algorithms, network protocols, distributed protocols, etc, could all be completed in Isabelle or Coq and then generate Haskell from the formal spec. For less-critical parts of the system you could use property based testing and various other "semi-formal" techniques which take less time but still add to the overall quality. I actually work in an agile environment that uses formal methods and it is possible!