Ancestors

Toot

Written by Paul Khuong on 2024-11-20 at 13:56

Passing around phantom typed proof witnesses as a revolutionary system design idiom that will change the world is peak googler.

=> More informations about this toot | More toots from pkhuong@discuss.systems

Descendants

Written by zwarich on 2024-11-20 at 14:52

@pkhuong Is there some additional context I am missing for this post?

=> More informations about this toot | More toots from zwarich@hachyderm.io

Written by Paul Khuong on 2024-11-20 at 19:36

@zwarich https://lwn.net/Articles/995814/ "this can reshape how we do software engineering"

=> More informations about this toot | More toots from pkhuong@discuss.systems

Written by Per Vognsen on 2024-11-20 at 20:06

@pkhuong @zwarich I saw the video (all the RustConf videos were uploaded yesterday it looks like) and I had a pretty similar reaction to you. This kind of thing would probably be a stronger sell to non-Rust or non-typed-FP programmers. I can see it being a strong sell to people who are used to traditional systems languages with very limited type systems.

=> More informations about this toot | More toots from pervognsen@mastodon.social

Written by Per Vognsen on 2024-11-20 at 20:07

@pkhuong @zwarich The specific trick in his talk where there's an unsafe LockBefore trait but a safe impl macro is kind of neat, I thought. It relies on the fact that trait resolution for conditional trait impls guarantees that the lock order is acyclic. (Although I admit I didn't think through all the details of that claim, so there could be problems with it.)

=> More informations about this toot | More toots from pervognsen@mastodon.social

Written by zwarich on 2024-11-20 at 23:14

@pervognsen @pkhuong As someone pointed out on Reddit, the solution (at least as described in the talk) also forbids acyclic diamonds: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=2d929295ddef42aca19cad7309f2f7b5

=> More informations about this toot | More toots from zwarich@hachyderm.io