I do not see what this has to do with Unix. The problem is not that programs interoperate or handle text streams, the problem is a) the supply chain issues in modern web-software (and thanks to Rust now system-level) development and b) that web applications do not run under user permissions but work for the user using token-based authentication schemes.
According to my experience, all the "zero-cost abstractions" from C++ most of the time make it more annoying to maintain and/or understand the code, especially with respect to resource management, introduce compatibility issues at the toolchain level, and - even when looking perfect in toy benchmarks - are often not even zero-cost (e.g. all the bloat the templates generate often hurts).
Even without Fil-C I do not think it is even clear that new software should be written in Rust. It seems to have a lot of fans, but IMHO it is overrated. If you need perfect memory safety Rust has an advantage at the moment, but if you are not careful you trade this for much higher supply chain risks. And I believe the advantage in memory safety will disappear in the next years due to improved tooling in C, simply by adding the formal verification that proves the safety which will work automatically.
Memory safety is absolute table stakes when it comes to formal verification. You can't endow your code with meaningful semantics if you don't have some way of ensuring memory safety.
That's far from trivial in Rust because of 'unsafe' blocks. There are approaches to verifying unsafe code in Rust, but formally verifying a Rust program is still likely to be significantly more complex than formally verifying, say, a Java program.
(And before someone says it: no you don't only have to verify the small amount of code in 'unsafe' blocks. Memory safety errors can be caused by the interaction of safe and unsafe code.)
Grepping for unsafe blocks doesn’t help that much for formal verification, because you have to verify all of the code.
The easiest way to see this is to note that ‘unsafe’ itself doesn’t have any semantics, so it can’t possibly allow anything to be proved that couldn’t have been proved otherwise.
It helps finding locations for possible flaws outside the type system soundness.
Now if we go discussing formal verification in general, even something like Dafny or Lean may fail, if the proofs aren't correctly written for the deployment scenario.
Just like one may still die while wearing helmets, airbags, and security belts, yet the casualties amount is much worse without them.
It helps a human armed with only a tool as crude as grep. But if Rust didn't have the requirement to mark unsafe operations with the 'unsafe' keyword, that information could trivially be added back automatically. If you're doing correctness proofs of realistic Rust code, you'd better already have tools that are at least capable of looking through your codebase for any instances of raw pointer access, etc.
There's a lot of mythology around Rust unsafe blocks. They're a useful lint, but they don't alter the fundamental safety properties of the language.
The mythology of unsafe blocks goes all the way back to ESPOL on Burroughs, still sold nowadays by Unisys, for customers that want OS security as the number one feature, before anything else.
It was also adopted by several systems and application programming languages outside C geology, until C# came to be, which is probably the first curly brackets language with unsafe code blocks.
The first error naysayers make on the eyes of SecDevOps, thus losing credibility points, is to focus too much on Rust, and too little on history of secure systems.
The first fundamental rule is to reduce attack surface, on C, and C++ (until and if profiles come to be), it is all over the place.
I don't see folks that usually post on HN or Reddit going to buy Astrée licenses, or integrate Frama-C into their development process.
I am not sure what point you're trying to make. Who are the 'naysayers', and what are they saying 'nay' to? And what do they have to do with anything I commented on?
Anyone that downplays unsafe code blocks as it was a Rust invention, available nowhere else.
Then uses it as argument, that since Rust has unsafe, there is no benefit over using C or C++ with a plain static analysis tool, but a basic one, because they are unwilling to actually use the ones people pay for on high integrity computing certifications.
Your comment to me seemed a bit going towards that direction.
Hmm, no, my comment didn't say any of those things. Specifically, I did not comment on (and do not care if) unsafe blocks are a Rust invention, and I made no comparison between Rust and C or C++.
Indeed, and this is why people who care about this are also proving memory safety in C. The issue is that we do not have good open-source tooling that specifically focuses on formal verification of memory safety in C.
Bounds checks have nothing to do with data races. GP is right, you can add bounds checks. Either using macros or (in C++) with templates and operator overloading.
Alas, in C or C++ you have mutable aliasing, so I'm afraid you do incur a potential data race because your bounds might alias. Be careful out there.
Also remember that in C++ you may get a reference in these cases and if you keep that reference rather than using it immediately now you also have a potential TOCTOU race because the reference was only valid when you did the bounds check.
With mutable aliasing the length might change even though the data you care about did not, and so adding the check means incurring a race which did not previously exist and which certainly the naive C programmer cannot see...
We can definitely mitigate this in the type system for most real world scenarios, but you don't mitigate problems you don't know about, so knowing is what's important.
Same reason any turing complete language needs any constructs - to help the programmer and identify/block "unsafe" constructs.
Programming languages have always been more about what they don't let you do rather than what they do - and where that lies on the spectrum of blocking "Possibly Valid" constructs vs "Possibly Invalid".
Reminds me of a commercial project I did for my old University department around 1994. The GUI was ambitious and written in Motif, which was a little buggy and leaked memory. So... I ended up catching any SEGVs, saving state, and restarting the process, with a short message in a popup telling the user to wait. Obviously not guaranteed, but surprisingly it mostly worked. With benefit of experience & hindsight, I should have just (considerably) simplified it: I had user-configurable dialogs creating widgets on the fly etc, none of which was really required.
The problem is not that society is too complexity but extremely unequal distribution of money. Those few that have most of it usually did not earn it by providing a useful service to society and for them it becomes a random investment game without consequences which creates additional winners that also never produced something useful.
Ok, then just cl.exe instead of gcc or clang. Completely different set of command line options from gcc and clang, but that's fine. C/C++ build tooling needs to be able to deal with different toolchains. The diversity of C/C++ toolchains is a strength, not a weakness :)
One nice feature of MSVC is that you can describe the linker dependencies in the source files (via #pragma comment(lib, ...)), this enables building fairly complex single-file tools trivially without a build system like this:
cl mytool.c
...without having to specify system dependencies like kernel32 etc... on the cmdline.
reply