| |
| ▲ | fhrow4484 a day ago | parent | next [-] | | > compile time abstract base class would enable compile time resolution of virtuals. so then i can do compile-time polymorphism What's wrong with static polymorphism that have been around for at least 31 years? (1995 per [1]). Also know as CRTP [2] Apart, of course, from ugly verbose compilation errors... And now c++23 "deducing `this`" [3,4] modern replacement which is supposed to improve compilation time and remove the verbose errors. [1] https://www.artima.com/articles/the-most-important-c-non-boo... [2] https://en.cppreference.com/cpp/language/crtp [3] https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2021/p08... [4] https://devblogs.microsoft.com/cppblog/cpp23-deducing-this/ | |
| ▲ | bluGill 2 days ago | parent | prev | next [-] | | Contracts are written such that the compiler can diagnose a detected violation if it wants to. However most contracts realistically need whole program analysis to diagnose and no compiler can do that - you want a separate static analysis for that. (this doesn't exist, but there is hope people start writing those) | | |
| ▲ | Cieric 2 days ago | parent [-] | | You sounds like you have more experience than me in this space (specifically contracts). I'm curious if you have any examples right off hand that would need whole program analysis. I need more examples to throw at my toy language that's not just another lock free work stealing queue. | | |
| ▲ | steveklabnik 2 days ago | parent | next [-] | | C++ contracts are not a compile-time construct, they're a runtime construct. Take the example from the article. The contract trips at runtime, not at compile time. | | |
| ▲ | bluGill 2 days ago | parent [-] | | The only required enforcement is runtime (even then it is optional). However nothing stops the compiler from detecting a violation at compile and time failing because of an error (or perhaps warning?) There is a lot of interest in static analysis enforcing contracts, but this will likely require some additions to the contract specification. | | |
| ▲ | steveklabnik a day ago | parent [-] | | I mean, what stops it is > this will likely require some additions to the contract specification. You need a lot more machinery to move this stuff to compile time, and not everything can be checked at compile time. The first example in the post would require you to validate that a <= v's len before indexing in order to be evaluated at compile time, for example. (Which of course is a runtime check anyway...) |
|
| |
| ▲ | bluGill 2 days ago | parent | prev [-] | | If I have more experience than you that means you have no experience at all. I've never used contracts in anything (not even a toy). I've been following contracts in hopes that they can be the next step in my quality journey, but I have no real world experience myself. By whole program analysis I mean you need the entire call tree of a function - stopping only when you can validate that the range of values is constrained to legal values. For some functions this is really simple, while for others the whole flow can be thousands of functions. | | |
| ▲ | Cieric a day ago | parent [-] | | Ah damn, okay. Long functions with a lot of sub calls is a known problem. I've been able to work around some of the issues tried to them by making every function an independent "compile unit." and then solving them each individually in the SMT solver. My experience in contract based programming is still relatively light, I won't lie there. The most I've had to do with contracts was ada, and even then it wasn't much. Everything else has been self enforced in languages without explicit support (and hence no compile time checking.) | | |
| ▲ | bluGill a day ago | parent [-] | | I'm no expert. my understanding though is that one of the reasons for contracts is solvers cannot possibly handle all the possible states of a program. if you can throw a contract in places they can break your whole program into subsets. That is, when analyzing a function and everything it calls, it just assumes the contract holds. And if everything works correctly according to contract and doesn't crash, well, they know that function is satisfied. Then they don't need to go back and say, well, everything calling that previous function only needs to meet the contracts, they don't need to prove everything that function calls is correct. This they can only do a subset of the full program analysis prove the whole program. | | |
| ▲ | Cieric a day ago | parent [-] | | Yeah, that sounds like the system I rediscovered. The only other thing I'm adding to try and lean more into that system are assertions(?) that are in the middle of a function, that can basically break it up into blocks on their own where the first block proves it true and the second block assumes it's true. So effectively the same thing as breaking it into 2 smaller functions. My main thing right now is, I'm fairly certain there is something wrong with my compiler, I'm a basically a novice in contracts, I'm intermediate in compilers, I'm a novice on SMT proofs, and I wrote the whole thing at this point using AI just to test an idea. So I'm just trying to throw everything I can at it to try and break it. I need to start building it again from scratch (without AI) so I can truly understand where it might break and what doesn't work. |
|
|
|
|
| |
| ▲ | Cieric 2 days ago | parent | prev | next [-] | | Yeah, I heard spark was used on a small component in the nvidia gpu firmware so others seemingly agree. I'm mainly in the user mode driver space so my ideas have been around having a kernel mode driver that (assuming a correctly functioning pc) can't crash and user mode drivers that can't be exploited (at least in the rop chain sense). I'm kind of picking ideas from other languages that I like zig's error handling, ada's contracts, rust's lifetimes (hopefully soon to be replaced with more contracts instead), and things like how you can use "gas" in lean to prove a loops will terminate. I'm mainly building it up with AI right now for experimentation, but I also can't really trust it to be correct either because of using AI. Once I settle on the syntax more and pump out a lot more tests, I'm probably going to rewrite the compiler by hand (hopefully in the custom language itself.) | |
| ▲ | jmalicki a day ago | parent | prev | next [-] | | How would this allow compile-time resolution of virtuals that was not possible before? Gcc can already do link-time devirtualization in some cases. | |
| ▲ | rramadass 2 days ago | parent | prev [-] | | You might want to take a look at Real-time C++: Efficient Object-oriented and Template Microcontroller Programming by Christopher Kormanyos for some ideas. Also take a look at David Crocker's Escher Technologies "Escher C Verifier and Escher C++ Verifier" (https://www.eschertech.com/products/ecv.php) and articles on "Verified Design-By-Contract" etc. linked to in my comment chain here - https://news.ycombinator.com/item?id=48544022 |
|
