4 ms·
> 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 c
by 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 agoSo 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 agoIf 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.