4 ms·
> Ada has had memory safety for decades Only with spark (i.e. formal verification). Which similar to other projects of this age (e.g. Rocq/How the compcert C c
by gpm 1y ago
> Ada has had memory safety for decades
Only with spark (i.e. formal verification). Which similar to other projects of this age (e.g. Rocq/How the compcert C compiler was implemented and proved correct) seems not to be low enough friction to get widescale adoption.
> not to mention Lisp, Java, etc. if you can live with garbage collection.
Like I said, high level languages that won't benefit from this at all have existed for ages... and the majority of software is written in them. This is one of the stronger arguments against it...
> But the Linux kernel (along with lots of other software which we would like to be reliable) is still mostly written in C, for better or worse.
Fil-C shows this can be solved at the software layer for things in this category that can afford the overhead of a GC. Which does mean a larger performance penalty than the hardware proposal, but also more correctly (since hardware changes can never solve unintended compilations resulting from undefined behavior).
The linux kernel is probably an example of an actual long tail project that would benefit from this for a reasonably long time though, since it's not amenable to "use a modified C compiler that eliminates undefined behavior with GC and other clever tricks" and it's unlikely to get rewritten or replaced with a memory safe thing quickly due to the number of companies collaborating on it.
- musicale 1y ago> Fil-C shows this can be solved at the software layer for things in this category that can afford the overhead of a GC. Mainline clang and g++ are also getting better with things like -fbounds-safety and -fsanitize=address. As I understand it, they typically have some overhead, but I'm willing to accept that overhead to have a kernel, web browser, etc. without memory errors. The decision that memory safety is too costly seems to have been made when CPUs were orders of magnitude slower than they are today. Hopefully hardware support will reduce the overhead to negligible proportions and enable memory safety as a default rather than an esoteric add-on or proprietary feature.
- pjmlp 1y agoNah, it was only a UNIX thing and C, see the world of systems languages and OS written in them outside Bell Labs. Had UNIX and C a price tag on their source code comparable to the competition, instead of a symbolic price and an annotated source code book, history would have played a different music.
- musicale 1y agoWhat competing OSes/languages do you think might have/should have surpassed Unix and C?
- pjmlp 1y agoVMS could have been one, for example. PL/I variants were being widely used, Apple was a Pascal fan, and is the company that actually created Object Pascal, not Borland. Modula-2 was around as well, unfortunely without an OS to go to market alongside it. The real question is, all things on equal footing regarding price, without access to source code to just type in/copy, what operating systems would people be willing to pay for.
- musicale 1y ago> Only with spark (i.e. formal verification) Ada's original memory safety was still a lot better than C's. As noted, PL/I was not 100% memory safe, but it was good enough to prevent buffer overflows in Multics.