Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Pony – High-Performance Safe Actor Programming

ponylang.io

Post reply on HN
Print view View original

151–159 of 159 posts

Re: Pony – High-Performance Safe Actor Programming

#151

Post by brundolf »

pjmlp wrote: post #144
brundolf wrote: post #133

Earlier quoted context omitted.

Worth noting that RefCell still enforces single-mutable-reference, it just does so at runtime . It lets you do things that could never be verified statically, but if you ever actually violate the condition, you'll get a panic (which is still better than memory unsafety).

Should be noted that this only works across threads. Nothing can be assumed regarding data races if it happens to be a shared value of some sort modified via IPC or other kind of APIs across multiple processes accessing the same resource.

That would require getting into unsafe { } code and passing along a raw pointer, wouldn't it? Nothing regarding safety can be assumed about unsafe code at all

Re: Pony – High-Performance Safe Actor Programming

#152

Post by pjmlp »

brundolf wrote: post #151
pjmlp wrote: post #144

Earlier quoted context omitted.

Should be noted that this only works across threads. Nothing can be assumed regarding data races if it happens to be a shared value of some sort modified via IPC or other kind of APIs across multiple processes accessing the same resource.

That would require getting into unsafe { } code and passing along a raw pointer, wouldn't it? Nothing regarding safety can be assumed about unsafe code at all

Nope, since when do you need to do that when using file IO or database connections?

The library code down at the bottom layer might do that, depending on how the bindings to the APIs are implemented, but it won't be necessarily exposed to the code you are writing yourself.

For example, doing SQL statements isn't unsafe { }.

Re: Pony – High-Performance Safe Actor Programming

#153

Post by brundolf »

pjmlp wrote: post #152
brundolf wrote: post #151

Earlier quoted context omitted.

That would require getting into unsafe { } code and passing along a raw pointer, wouldn't it? Nothing regarding safety can be assumed about unsafe code at all

Nope, since when do you need to do that when using file IO or database connections? The library code down at the bottom layer might do that, depending on how the bindings to the APIs are implemented, but it won't be necessarily exposed to the code you are writing yourself. For example, doing SQL statements isn't unsafe { }.

What I'm not seeing is how the actual value contained inside a RefCell would get modified out from underneath your code without going through its checked methods, unless something has a raw pointer directly to its contents

Re: Pony – High-Performance Safe Actor Programming

#154

Post by pjmlp »

brundolf wrote: post #153
pjmlp wrote: post #152

Earlier quoted context omitted.

Nope, since when do you need to do that when using file IO or database connections? The library code down at the bottom layer might do that, depending on how the bindings to the APIs are implemented, but it won't be necessarily exposed to the code you are writing yourself. For example, doing SQL statements isn't unsafe { }.

What I'm not seeing is how the actual value contained inside a RefCell would get modified out from underneath your code without going through its checked methods, unless something has a raw pointer directly to its contents

Because you aren't looking at it from the context of data races anywhere on the application, and focusing on RefCell alone instead.

Yes, Rust prevents data races when several threads try to modify a memory location inside the same process.

This is just a special case of data races, which may take several forms.

If several processes, or even threads are accessing an external resource, like a database, each of them can issue UPDATE statements on the same record, and it is impossible to validate which value you will get back, unless it is done inside a proper transaction block.

Ensuring that a SQL data race doesn't happen, might be critical, e.g. several people to the same plane seat, yet there is nothing on the RefCell or not using unsafe {} that can enforce it.

I would advise to read the "Data Races and Race Conditions" chapter of Rustonomicon regarding what guarantees Rust actually provides, anything else is up to the programmer to take care they don't happen.

https://doc.rust-lang.org/nomicon/races.html

Re: Pony – High-Performance Safe Actor Programming

#155

Post by kirugan »

spooneybarger wrote: post #6
threatofrain wrote: post #3

Prior discussion from 4 months ago. https://news.ycombinator.com/item?id=24398469 Has anything new happened to the language?

pony core team member here. There has been nothing large or dramatic in the last 4 months. We are plugging away at improving ecosystem tools, the runtime, and a variety of other things; incremental improvement. We spent money from our open collective account recently to purchase a couple Apple Silicon mac minis so we can get pony working on Apple Silicon machines. That's probably the biggest "outside the community" n…

Do you need any help with Apple Silicon transition? I've purchased a new mac mini recently and looking for an open-source project to contribute.

Re: Pony – High-Performance Safe Actor Programming

#157

Post by ProfHewitt »

Consider the following example:

    open:[String]->FileDescrptor

    ReadWrite restriction FileDescriptor to 
                                  read -> Item,
                                  write[item] -> Void

    ReadWriteOpen:[String]->ReadWrite 
     [aString] |-> 
                 aDescriptor  aDescriptor.read,
                              write[anItem] |-> aDescriptor.write[anItem] 

    fd
Now we have an Actor fd that can only do reads and writes on

the opened file.

Consequently, fd is just one thing in Actors as opposed to

kind of being two separated things in Pony.

Is the separation in Pony really a good idea?

Re: Pony – High-Performance Safe Actor Programming

#158

Post by throwaway894345 »

pjmlp wrote: post #146
nextaccountic wrote: post #80

Earlier quoted context omitted.

> And many times the borrow checker is completely inadequate at preventing data races (frequently the case with distributed computing). The borrow checker (in safe rust) always[0] prevents data races. It can't, however, prevent race conditions (but neither can pony do[1]) [0] https://doc.rust-lang.org/nomicon/races.html [1] https://www.ponylang.io/faq/#data-race

> The borrow checker (in safe rust) always[0] prevents data races. As long as those data races originate from threads, it cannot prevent data races across processes, for example: - Modifying the same file location - Modifying the same table cell without transactions - Talking to the same IO port - Data sharing between CPU and GPU

In fairness to the OP, the link they cited defined "data race" explicitly and narrowly as race conditions on memory which I think makes all of your bullets out of scope, but also neuters the original claim pretty considerably.

Re: Pony – High-Performance Safe Actor Programming

#159

Post by haskellandchill »

hntemppony wrote: post #130
haskellandchill wrote: post #52

Anyone know the judgement rules behind the interesting parts of Pony's type system? I'm about to crack the dissertation to see what's up but would love a concise description. https://www.ponylang.io/media/papers/a_prinicipled_design_of...

The interesting parts: Capabilities describe both uniqueness and read-write ability. `iso` is fully unique and hence sendable, `trn` and `val` are write-unique (but `val` is also sendable since it isn't writable). The `tag` capability allows identity/message sending and is fully sendable Recover blocks and automatic receiver recovery allow creation/usage of isolated data if only sendables are used from the external e…

Could dependent types model capabilities? Would never be as ergonomic as Pony, but I'm wondering about expressive power of dependent types compared to indexed judgement rules or linear judgement rules.
Post reply on HN