4 ms·

This is a well put argument and I won't attempt to go into all of your points more than to say that I pretty much agree, and step back some from my argument tha

by hvs 17y ago

This is a well put argument and I won't attempt to go into all of your points more than to say that I pretty much agree, and step back some from my argument that formal analysis necessarily helps abstraction. I guess my point was that in order to for larger and larger abstractions to be implemented, there needs to be trust in those abstractions. One problem that you point out is that right abstractions can be difficult to come up with, which will not be improved by formal analysis. The other problem is that as you build greater and greater abstractions on top of each other, "holes" in those abstractions can cause odd problems in the system. Here, formal verification can at least provide the level of trust that the abstraction works exactly how you expect it to and can implement your system on top of it without concern for odd effects. One analogy could be with the computer hardware on which software is implemented upon. It goes without saying that while software is often expected to have flaws, the hardware is essentially assumed to be flawless for all intensive purposes. This isn't a perfect analogy because you have firmware, etc, but hopefully it illustrates my point. You don't worry about the processor not correctly implementing add ax, bx It is taken as a given. At almost no point in software development today can you make that assumption about any code. Maybe formal analysis isn't the solution to this particular problem. I do think it is important to research the topic as fully as we can to figure out if it is or isn't.

10ren 17y ago
"It is by logic we prove, it is by intuition that we invent" - Henri Poincaré I emphasized the invention, but you're quite right that we also need the proving. I agree with your hardware example (things like the Pentium bug are rare...), but I think we similarly rely on other layers (OS, languages, libraries), though I concede with eroding confidence as we rise. For hardware, it's also that we have more trust in the common pathways (Dijkstra wouldn't like it - it all should be perfect. I can relate to this, but that's not how it is - today, anyway). Popular hardware is used extensively, and very importantly, I think it tends to be designed to be pretty flat, in that almost all of it gets exercised by almost all uses (i.e. there are few rare pathways). So flaws will show up quickly. We also don't worry about the language not correctly implementing a+b So I think you can make that assumption about code, if the code is well exercised (e.g. in a fundamental part of the code in the language runtime). Concessions: Dr. Gosling apparently did write some (informal) proofs for Java, but it was in the byte-code verifier, not for the typical language stuff. But I've heard that Intel does some formal verification :-). I agree that formal analysis is a worthwhile endeavour. I just wish they would do more work on interesting, useful problems. It used to be that computer scientists would invent something incredibly cool (like Boyer-Moore substring matching, or arithmetic coding), and then also prove it (well, really, prove some specific qualities about it). But these days, there seems to be a lot of proving things just because they can be proven - not because they are worthwhile proving. It's quite... insular. They focus on proof, not invention.

by hvs 17y ago

10ren 17y ago

"It is by logic we prove, it is by intuition that we invent" - Henri Poincaré I emphasized the invention, but you're quite right that we also need the proving. I agree with your hardware example (things like the Pentium bug are rare...), but I think we similarly rely on other layers (OS, languages, libraries), though I concede with eroding confidence as we rise. For hardware, it's also that we have more trust in the common pathways (Dijkstra wouldn't like it - it all should be perfect. I can relate to this, but that's not how it is - today, anyway). Popular hardware is used extensively, and very importantly, I think it tends to be designed to be pretty flat, in that almost all of it gets exercised by almost all uses (i.e. there are few rare pathways). So flaws will show up quickly. We also don't worry about the language not correctly implementing a+b So I think you can make that assumption about code, if the code is well exercised (e.g. in a fundamental part of the code in the language runtime). Concessions: Dr. Gosling apparently did write some (informal) proofs for Java, but it was in the byte-code verifier, not for the typical language stuff. But I've heard that Intel does some formal verification :-). I agree that formal analysis is a worthwhile endeavour. I just wish they would do more work on interesting, useful problems. It used to be that computer scientists would invent something incredibly cool (like Boyer-Moore substring matching, or arithmetic coding), and then also prove it (well, really, prove some specific qualities about it). But these days, there seems to be a lot of proving things just because they can be proven - not because they are worthwhile proving. It's quite... insular. They focus on proof, not invention.