I do think the ideal kind of memory safe language either has no "unsafe", or has an "unsafe" feature that only needs to be used in super rare an obscure cases (Java is like that, sort of).
Fil-C has no "unsafe", so in that sense Fil-C is safer than Rust. You don't need an escape hatch if the memory safety guarantees are dialed in just right.
Someday, man
If I told you that I have a snippet of machine code that:
- obeys the ABI of your safe language (ie it has exactly the calling convention that safe language uses)
- corresponds exactly to a function body whose signature is T->U (or whatever, different safe languages have different function type syntax)
- obeys the language’s type system.
Then you could run an abstract interpreter to check that the machine code follows that type system. Simple example: given the above claims, if we further assume that the host language impl puts argument one into register 5, and the first argument’s type is “pointer to an array of bytes”, and we know that arrays have a 64-bit length prefixed to the start, then the abstract interpreter would just need to check that any deref of register 5 is preceded by a bounds check on whatever was loaded at offset -8 from register 5. And so on, for every possible thing you can do in the language.
Then the JIT would just have to make sure it puts checks in all of the places that the absint expects them. If the absint fails, then the machine code is rejected.
I am trying out a couple of new directions, e.g. generating more of the tiers from a more abstract description, constantly shrinking the amount of hand-written compiler/interpreter code. My hard requirement is the end result has to be pretty darn close to what I'd write by hand.
One thing I am thinking about now is how to make more use of the implementation language's (e.g. Virgil) compiler to be able to paste together machine code templates gotten from writing in the implementation language. Think copy-and-patch compilation, but as language primitive. E.g. "please emit an inlined copy of the machine code for this function (first-class ref to said function) into memory here, under this ABI".
You say that and then you describe exactly what I would have used as a solution: copy and patch.
Just have the checker check the templates that the baseline JIT is stitching together and then have a safe way to ask for the prechecked templates to be stitched together.
Bunch of details in getting that right obviously, but it doesn’t seem impossible.
> Just have the checker check the templates that the baseline JIT is stitching together
Sure, from my second paragraph, the templates it's using could be opaque things it got from requesting the static compiler generate a template from a first class function ref (at compile time), in which case the verification has already been done.
Toy systems, yes. Hey, I too, think CircuitPython is really neat. But I'm skeptical someone would base a PLC (or similar) on it.
The James Webb Space Telescope runs JavaScript, apparently [1].
[1]: https://www.theverge.com/2022/8/18/23206110/james-webb-space...
C got its performance fame thanks to optimizing compilers that abuse UB semantics.
Microsoft team on .NET, especially the great Stephen Toub blog posts, has been showing off how much performance can be squizzed out of a managed language compiler toolchain when people actually care.
Also lets not forget Apple only moved away from Object Pascal due to an internal team doing MPW initially as kind of submarine project, due to their UNIX roots, and still their focus was C++, not C.
But Fil-C objects (at least for now?) only seem to allow one single capability type, and that capability grants unrestricted read/write access to the object’s bytes.
I wonder if one could build a handle system in Fil-C that would allow this to be extended. Or if a different variant of a Fil-C-like system could distinguish between pointers with different access levels to an object and could allow only the correct piece of trusted code to increase the permission of a pointer.
What I mean by that is: the memory safety issues of C are a total dumpster fire, while whether a number is even or not (and whether you can prove that) is maybe like icing on the dumpster fire. It just doesn’t matter by comparison.
So I want to decisively fix the memory safety issues and not lose focus.
Fil-C doesn't necessarily have to run in production. It just needs to catch the bugs, e.g. by making it easy to fuzz C code compiled via Fil-C.