4 ms·

There appears to exist a guy with a formal background who is interested in submitting a paper about formal verification and static analysis and stuff. Impressiv

There appears to exist a guy with a formal background who is interested in submitting a paper about formal verification and static analysis and stuff. Impressive work, but I really don't know what to take home from the existance of this, or what argument this supports. In my sibling post I merely want to illustrate that all these concerns have little bearing on my day-to-day work (which mostly doesn't need to be certified, and is not related to the defense industry or similar). Some of these I perceive as FUD, as said I know that you can provoke these situations but I've never personally encountered nasal daemons in practice, and I feel quite productive, am not spending a lot of time on bugs, so why bother.

tialaramex 2y ago
Gabriel Dos Reis is specifically an old colleague of Bjarne Stroustrup (they worked at the same University, Texas A&M) who is now working for Microsoft on C++ tooling and so on. So, one way to understand these papers is that Microsoft (at least some parts of it) thinks unsafe Contracts are worse than no Contracts. Now, would that mean they just won't implement an unsafe Contracts feature shipped in a C++ 26 document? Maybe. Would these fixes get it over the line? Maybe.
- jstimpfle 2y ago
  I'm taking a closer look, but from the looks of it I'm not a fan of adding yet another sub-language with differing syntax and semantics. This leads to complexity, it's a path to madness. Without being involved -- I have no intention using any of these Contracts in whatever form. I will say though that I wouldn't care if there is UB in the contract language (just like there is in the normal language). I would prefer the variant with UB if it is simpler and more aligned with the language core. Removing the UB here is an academic exercise. Safety absolutists are uncompromising about the goal of correctness and provability. They are blind to the pragmatic issues created by the idealism. Contracts in either form could probably improve correctness by a lot, like 99% or whatever. So why should I care about the paper which could in theory bring the remaining 1%? It doesn't affect me pragmatically. The flaw with either is that this is only in theory. In practice, I will never create enough formal contracts in to significantly improve correctness. Whatever system it is. Why? The costs are just too damn high, the only way to achieve 100% correctness when considering also pragmatic concerns, is to just not write any code. My approach of just coming up with a simple design (not in code), trying to implement it in the most straightforward way, and fixing the code until it works, as described in my other comment, seems to have achieved something very close to correctness (maybe even 100%? Probably not). Again, I'm not saying that UB is good or should be tolerated. I don't want it in my programs and if I find an instance of UB I'll try hard to get rid of it. However there is a reason why UB exists in C/C++ (as well as many other languages that may not have as much of it, but still have a lot of it even when not defined explicitly). And alternative approaches, trying to prevent UB mechanically, come with a cost that may not be worth it depending on what you're working on. I feel strongly like it isn't worth it for me. If you're building a fully verified or certified product, tradeoffs are likely different. If we're citing big names, here is a well known person describing their view, which I find myself agreeing a lot with. https://www.youtube.com/watch?v=EJRdXxS_jqo https://www.youtube.com/watch?v=EJRdXxS_jqo
- rurban 2y ago
  Gabi is the Visual C compiler maintainer, not just tooling. The only sane person in the C++ ISO committee (_besides the sdcc maintainer, who has no power at all_).

tialaramex 2y ago

Gabriel Dos Reis is specifically an old colleague of Bjarne Stroustrup (they worked at the same University, Texas A&M) who is now working for Microsoft on C++ tooling and so on. So, one way to understand these papers is that Microsoft (at least some parts of it) thinks unsafe Contracts are worse than no Contracts. Now, would that mean they just won't implement an unsafe Contracts feature shipped in a C++ 26 document? Maybe. Would these fixes get it over the line? Maybe.

jstimpfle 2y ago
I'm taking a closer look, but from the looks of it I'm not a fan of adding yet another sub-language with differing syntax and semantics. This leads to complexity, it's a path to madness. Without being involved -- I have no intention using any of these Contracts in whatever form. I will say though that I wouldn't care if there is UB in the contract language (just like there is in the normal language). I would prefer the variant with UB if it is simpler and more aligned with the language core. Removing the UB here is an academic exercise. Safety absolutists are uncompromising about the goal of correctness and provability. They are blind to the pragmatic issues created by the idealism. Contracts in either form could probably improve correctness by a lot, like 99% or whatever. So why should I care about the paper which could in theory bring the remaining 1%? It doesn't affect me pragmatically. The flaw with either is that this is only in theory. In practice, I will never create enough formal contracts in to significantly improve correctness. Whatever system it is. Why? The costs are just too damn high, the only way to achieve 100% correctness when considering also pragmatic concerns, is to just not write any code. My approach of just coming up with a simple design (not in code), trying to implement it in the most straightforward way, and fixing the code until it works, as described in my other comment, seems to have achieved something very close to correctness (maybe even 100%? Probably not). Again, I'm not saying that UB is good or should be tolerated. I don't want it in my programs and if I find an instance of UB I'll try hard to get rid of it. However there is a reason why UB exists in C/C++ (as well as many other languages that may not have as much of it, but still have a lot of it even when not defined explicitly). And alternative approaches, trying to prevent UB mechanically, come with a cost that may not be worth it depending on what you're working on. I feel strongly like it isn't worth it for me. If you're building a fully verified or certified product, tradeoffs are likely different. If we're citing big names, here is a well known person describing their view, which I find myself agreeing a lot with. https://www.youtube.com/watch?v=EJRdXxS_jqo https://www.youtube.com/watch?v=EJRdXxS_jqo
rurban 2y ago
Gabi is the Visual C compiler maintainer, not just tooling. The only sane person in the C++ ISO committee (_besides the sdcc maintainer, who has no power at all_).