afaik, the c is handwritten for performance reasons, and is manually proven to be a refinement of the executable haskell model. the haskell is then proven to be a refinement of an abstract, more succinct spec.

Fine! Now we have a way to write guaranteed safe C code.

It requires quite a lot of qualification from the development team, though.

if ur fine with writing 4 lines of code a day from an expert...i guess

With endless bug-hunting in hastily-written C code, it could be fewer than 4 lines a day of completed code. (I hope nobody actually does so poorly, except while learning C.)

of course, with unverified code, "completed" means absence of evidence of bugs, not evidence of absence.

unfortunately, it's unsound https://github.com/mcoblenz/Bronze/issues/2

That’s an evil problem to have. Let’s say you derive two references to a GC’d object (this can easily happen accidentally in a graph-like data structure) and pass them both as parameters to a function. I’ve looked at disassembled Rust code before. Given how aggressively the compiler optimizes based on the guarantees around & and &mut, I’d be surprised if this system compiles any non-toy programs correctly at all.

how about an actual computer services shop as a front?

AND they could install spyware on the PCs....vertically integrated, as it were

i eagerly await the day when chrome realizes their current situation of being written in a memory unsafe language is untenable. it seems like they're still in denial, but they're slowly realizing https://docs.google.com/document/u/1/d/e/2PACX-1vSt2VB1zQAJ6...

is that saying anything if microsoft is basically eternal? what, you think the company that makes excel and windows is gonna go out of business any time soon?

The usual route is becoming irrelevant. Windos failed to achieve relevance in mobile and cloud, and desktops become less relevant every day. If at some point you don't need MS to do excel anymore, MS becomes irrelevant there, too.

There are still Burroughs, Univac, and Honeywell computer companies, in a way, but they attract no attention.

if there was a production-grade memory-safe language with similar performance, i would also advocate for it. it's less that rust is good, and that memory unsafety is bad.

let's check out https://googleprojectzero.blogspot.com/2021/12/a-deep-dive-i..., which has probably been used to enable "crimes against humanity". integer overflow results in undersized allocation which is indexed out of bounds. if c++ had either overflow checks or bounds checking as the default, how likely is this bug to happen?

it's more like being written in a memory-unsafe language is an anti-feature.

This. I don’t really care about replacing Java or Python or Go with Rust (any perf difference might not be worth the extra effort), but evidence has been mounting for my entire career that we must leave C and C++ behind if we’re ever going to arrive at a platform that works reliably.

the worst part is that testing might give something that is reliable against non-malicious inputs, and then explode given malicious ones. actually, that's not the worst part. the worst part is when nothing seems to occur on a malicious input, but actually rce is occurring https://googleprojectzero.blogspot.com/2021/12/a-deep-dive-i....

> I have spent strictly more time in the last five years filing compiler bugs than chasing memory usage errors in my C++ code.

maybe because your code isn't worth having people actively attack?

My experience is the same as theirs. In recent years I've run into more compiler bugs than memory bugs in the large, complex C++ code bases I work with.

It makes sense. A common use case for C++ today is writing high-performance software, where the software architecture is likely to be schedule-driven (e.g. thread-per-core, userspace I/O, etc). In these cases, you see minimal heap allocation, shared structures, or locking. Modern C++ is pretty safe by default for this; it allows you to do unsafe things, and to do safe things that the Rust compiler deems unsafe, but there isn't a cabal forcing people to write non-idiomatic unsafe C++ code in software architectures where the code is naturally almost entirely single-threaded and with few heap allocations.

The most insidious bugs I see in modern C++ code bases are scheduling bugs e.g. logical or behavioral edge cases due to pure async execution, which can be very subtle. Rust doesn't help with that.

As someone that doesn't work in this space, I'm interested in the schedule-driven architectures that you mention. Do you know of any talks where they explain this or, if you have some time, could you explain how the approach has changed over the past couple of decades, what architectures were common in the past, their issues, and what issues this fixes?

is your code as actively attacked as a web browser or iOS?

Good luck getting Apple to rewrite iOS in Rust, so at least that part of your argument is pointless.

no, just clarifying the difference between not encountering bugs and not having them.

Then you should have said that. This actually makes sense.

Apart from that, everyone even half competent would know that and make a trade-off involving other factors. Being dogmatic about a single facet isn't helpful.

the trade-offs are probably made to maximize profits for shareholders, and security is deprioritized as a negative externality.

i wouldn't mind C if every program written in it was written to the standard of seL4, but alas, that isn't the case, and usually it's not even close. i'm also quite sure that getting even close to it would make you want to use another language instead.