2 ms·

I agree with what you say. I do not see the relation between working hard or picking difficult languages or frameworks and the points you make. But generally I

I agree with what you say. I do not see the relation between working hard or picking difficult languages or frameworks and the points you make. But generally I agree with you here. That was also the reason I mentioned the word balance in my comment; I was raised by a Dijkstra student (my father) and proofs were mentioned a lot; I studied under students of Dijkstra at the TUE when I went to uni. These people all would say you do not work 'hard enough' if you did not provide proof for your code and I am pretty sure you do not. Which means you balance your, in that respect (!), very sloppy code which you write very fast compared to when you add proofs, with stability and security which you and your users value? So why do you not work harder and provide 100% covering formal verification of your code? Because that would make little sense in most cases. So you balance.

fiedzia 10y ago
> if you did not provide proof for your code and I am pretty sure you do not. I am not entirely there yet, but it is where I am aiming. I may not prove total correctness, but I already am close to proving (or make very likely) absence of certain types of bugs that comes from my compiler and language guarantees. > So why do you not work harder and provide 100% covering formal verification of your code? Because that would make little sense in most cases. I'd like to, but its not practical yet for me. And I balance. But every now and then we are getting tools that shift the balance a bit further, and the boundary of what's practical and acceptable moves too.
- tluyben2 10y ago
  So we agree largely again :) Basically it makes no sense to go far beyond what users ever want to pay; you will have to balance that. For projects that might end up there, I prove things (with Coq). Never 100% because it is really a lot of work to provide even proofs for small parts of the code base. But vital parts yes, for fun and profit. In that order.
  - fiedzia 10y ago
    If you are using Coq at all my post is not directed to you :-) Right now I'm perfectly happy if software I rely on doesn't have trivial security vulnerabilities, does not fail silently and does not damage my data, anything above that is a bonus. It may not be much, but it still far above industry standards in many areas.

fiedzia 10y ago

> if you did not provide proof for your code and I am pretty sure you do not. I am not entirely there yet, but it is where I am aiming. I may not prove total correctness, but I already am close to proving (or make very likely) absence of certain types of bugs that comes from my compiler and language guarantees. > So why do you not work harder and provide 100% covering formal verification of your code? Because that would make little sense in most cases. I'd like to, but its not practical yet for me. And I balance. But every now and then we are getting tools that shift the balance a bit further, and the boundary of what's practical and acceptable moves too.

tluyben2 10y ago
So we agree largely again :) Basically it makes no sense to go far beyond what users ever want to pay; you will have to balance that. For projects that might end up there, I prove things (with Coq). Never 100% because it is really a lot of work to provide even proofs for small parts of the code base. But vital parts yes, for fun and profit. In that order.
- fiedzia 10y ago
  If you are using Coq at all my post is not directed to you :-) Right now I'm perfectly happy if software I rely on doesn't have trivial security vulnerabilities, does not fail silently and does not damage my data, anything above that is a bonus. It may not be much, but it still far above industry standards in many areas.