4 ms·
What do Idris and Agda have to do with safety? They have a GC RUNTIME; Rust leverages the type system to get ergonomic, safe and fast code without a runtime.
by Ar-Curunir 10y ago
What do Idris and Agda have to do with safety? They have a GC RUNTIME; Rust leverages the type system to get ergonomic, safe and fast code without a runtime.
- krapht 10y agoProgram correctness (safety) is way more than just the memory access guarantees Rust gives you.
- pjmlp 10y agoIdris does not have one exclusively. Allocations can be removed just like in Rust thanks to uniqueness types: http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html?highlight=memory http://docs.idris-lang.org/en/latest/reference/uniqueness-ty... Also funny that you mention ergonomics, given that improving the current state is one of the main goals of 2017's roadmap.