#Is it possible to create custom allocators?
1 messages · Page 1 of 1 (latest)
thats kind of one of the ideas
Afaiu, Zig attempts to replace C in all use cases except 1. verification (Misra compcert C => C compiler implementation and verification is simpler, verifying Sema.zig looks unfeasible to me) and 2. bootstrapping from 0 (bare CPU instructions => Zig requires bootstrapping to a working C compiler first).
Afaiu, case 1 implies SIL4 (requiring state of the art verification) is out of reach.
Except, if one would do manual verification of the IR (Air or Mir) + phases from IR to machine code or binary semantics (more costly).
Mhm. There are 2 use cases of C on verification: 1. Generated code with C as target language (for example simulink can generate C code or other "pure" languages [without io except allocation]) and 2. (annotated) C as source language (for example compcert C). I was mostly referring to case 2, as case 1 looks like it means no significant difference to me.
At least to me, it looks like the second one would require an alternate compiler implementation, because Sema.zig with all the comptime semantics are too complex to verify + all the work be "redone" from compcert C.
I dont think this is viable to think about before there is a final "verifiable C" standard in sight for academia to focus/push, which means to clarify pointer semantics (aliasing rules) + weak memory model for sound concurrency optimizations. The latter is especially hard, because global + local optimizations can affect another and the explosions of possible choices. See also https://github.com/ziglang/zig/issues/6396 for the scattered details.