DIP1000

[Andrei Alexandrescu via Digitalmars-d]

On 8/30/16 3:42 PM, Timon Gehr wrote:
> On 30.08.2016 18:12, Andrei Alexandrescu wrote:
>> I'd like to initiate collaboration on an effort to do DIP1000 rigorously.
>>
>> First we need to reduce D to a bare subset that only has integers,
>> structs, pointers, and functions. That's a working subset of actual D
>> code. The grammar I have in mind is at http://erdani.com/d/DIP1000.html.
>> ...
>
> - Missing a production rule for ArgumentList.
>
> - There is no ParameterList of length three or more.
>
> - 'return' annotations missing.

Cool, thx.

> I'd just actually deallocate the memory slots when their lifetime ends
> and then prove type safety. (This implies in particular that the
> accessed addressed are still allocated for all dereferencing expressions.)
>
>> The model for typing, evaluation, and proofs is at
>> https://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf.
>
> Typing and proofs yes, to some extent, evaluation not really. This paper
> does not allow mutation and does not model memory/aliasing. One
> possibility would be small-step semantics with an explicit heap. (The
> heap would be infinite and never reuse memory slots between allocations.
> This way, memory slots can be reliably marked as already deallocated.

Yah. There are a few papers on modeling heaps, it's not difficult.

> The stack would not need to be modeled separately, just allocate non-ref
> parameters and locals when entering the function and deallocate them
> when the function exits.)

Ah, neat. Didn't think of that.

Thanks. I'm embarking on a trip right now, but will get to this as soon 
as I can.


Andrei