[quic5]

That is absolutely true. But but you can write memory-bug-free code in Zig but you cannot prevent heap allocations in most of the languages listed in the article, making it outright impossible to write certain software in them.

[grumpyprole]

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]

As 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]

A 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).

[memefrog]

You can't prove it in Rust either.

[ArtixFox]

formalized 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.