Temporally safe by default

[Richard (Rikki) Andrew Cattermole]

On 05/04/2024 1:32 AM, Dukc wrote:
> On Thursday, 4 April 2024 at 06:45:44 UTC, Richard (Rikki) Andrew 
> Cattermole wrote:
> 
>>> Can you please write a code example or two? Doesn't have to be 
>>> anything with a nailed-down syntax, but it's really hard to be sure 
>>> what you're suggesting without one.
>>
>> Okay so you need something a bit bigger picture for temporally safe?
>>
>> My way of working would mean I would need to solve isolated and then 
>> temporally safe before I can do that.
>>
>> It might be a while before it all comes together for me to be able to 
>> do it concretely.
> 
> I mean, given you're posting this as a new thread in the DIP ideas 
> forum, I'm assuming you have a language improvement idea to present and 
> want some informal feedback for it. But I don't get from your posts what 
> exactly you're proposing, only that it's some sort of improvement to 
> `@safe`.

Okay yes, you want some big picture overview.

Temporal safety is about making sure one thread doesn't stomp all over 
memory that another thread also knows about.

So this is locking, ensuring only one thread has a reference to it, 
atomics ext.

Moving us over to this without the edition system would break everyone's 
code. So it has to be based upon this.

So the question of this thread is all about how do we annotate our code 
to indicate its temporally safe and how does it map into older editions 
view of what safe is. There is at least three different solutions to 
this that I have come up with.

Escape analysis wrt. DIP1000 is only a very small part of such a system. 
But it all plays together to give us what is known as program security.

Program security is what the CS field has been working towards since the 
80's. Its about guaranteeing that a program will work as expected 
guaranteed. We are no where near that, it'll need a proof assistant for 
full blown program security, however temporal safety will get us most of 
the way there.

I know Walter has seen the writing on the wall for PL's if they don't 
have it ~5 years ago. Hence DIP1000 and @live. However I don't know how 
far along the path he has gone. I'm waiting on him talking with Adam 
Wilson this month to find that out to know how to proceed with type 
state analysis (which is a building block to make it all work nicely 
together).