2 ms·
Sure one can write memory-bug-free code in x86 assembly too. But how can you prove it? ATS is an example of a low-level systems language where you can prove it.
by grumpyprole 3y ago
Sure one can write memory-bug-free code in x86 assembly too. But how can you prove it? ATS is an example of a low-level systems language where you can prove it.
- ObscureScience 3y agoAs Zig promises "not hidden allocation", I assume you can build your allocator in Rust and then use it for all memory allocation in Zig.
- lmm 3y agoA function that doesn't allocate doesn't mean it's safe. (Indeed if anything the opposite is more likely - copying is safe, if slow, writing to something that was passed in tends to be what breaks).
- ArtixFox 3y agoformalized subsets of x86 assembly exist. Coq can be used as a macro assembler. tools to work with llvm ir exist, x86 can be raised up to llvm ir and proved, kinda bad way tho.
- memefrog 3y agoYou can't prove it in Rust either.