Hongwei Xi said...
On Tue, 21 Jan 2014, Kiwamu Okabe wrote:
>>Hi Hongwei,
>>
>>On Tue, Jan 21, 2014 at 9:43 AM, Hongwei Xi <hwxi@bu.edu> wrote:
>>> Seriously, I don't think that Rust is really designed to do the kind of
>>> low-level programming you want to do. There is still a big gap between
>>> Rust and C in terms of run-time semantics. This gap will not go away for
>>> free. In order to bridge it, you need to have run-time support. Having
>>> this kind of run-time support is not just giving your bigger code size;
>>> it has all sorts of implications that are difficult to predict.
>>
>>Umm... But Rust can strip the runtime.
>>See below.
>>
>>https://github.com/neykov/armboot
>>
But type-safety is also stripped away as well?
I am not a Rust programmer. I am curious to know what kind of safety you
can get when writing Rust programs this way.
At the end, the bottom line question is this:
Given a pointer p, how does rustc know whether *p (dereferencing p) is safe
or not?
In ATS, the answer is that a proof is needed in order to dereference a
pointer:
ptr_get (pf | p)
ATS allows you to construct this proof explicitly when needed. In Rust,
this proof is constructed automatically and implicitly by the typechecker.
But constructing such a proof automatically in low-level programming is
a unpredictable business.
I think you can find this out if you try to translate a C-style quicksort
or binary search into Rust.
Hongwei Xi said...