8 ms·

> How am I trading those? If you choose the easiest thing for you instead of the one that provides some guarantees of quality for me, I may be the one who lose

by fiedzia 10y ago

> How am I trading those? If you choose the easiest thing for you instead of the one that provides some guarantees of quality for me, I may be the one who loses something here. > How would they care if the end result for them is the same? There is no issue if that's the case, problem is that it often isn't. > I use Clojure as I have a lot of experience there; how is that trading quality for convenience? I am not talking about this situation. You are clearly making well informed choice (and sufficiently good one for me). Functional languages do not fall into the "easy" scope I had in mind. > Also: why do you want me to work 'harder'? So that I am not left with never ending bug chasing or exposed customer data. I expect you to adhere to certain quality standards, not to bash some code as fast at possible for your convenience. Just that.

tluyben2 10y ago
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.

by fiedzia 10y ago

tluyben2 10y ago

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.