#prog #rust #article
Очень хорошая демонстрация пользы от type-level наворотов.
The Rust language offers a promising approach to safe systems programming based on the principle of aliasing XOR mutability: a value may be either aliased or mutable, but not both at the same time. However, to implement pointer-based data structures with internal sharing, such as graphs or doubly-linked lists, we need to be able to mutate aliased state. To support such data structures, Rust provides a number of APIs that offer so-called interior mutability: the ability to mutate data via method calls on a shared reference. Unfortunately, the existing APIs sacrifice flexibility, concurrent access, and/or performance, in exchange for safety.
In this paper, we propose a new Rust API called GhostCell which avoids such sacrifices by separating permissions from data: it enables the user to safely synchronize access to a collection of data via a single permission. GhostCell repurposes an old trick from typed functional programming: branded types (as exemplified by Haskell's ST monad), which combine phantom types and rank-2 polymorphism to simulate a lightweight form of state-dependent types. We have formally proven the soundness of GhostCell by adapting and extending RustBelt, a semantic soundness proof for a representative subset of Rust, mechanized in Coq.
plv.mpi-sws.org/rustbelt/ghostcell
(thanks @dogeshibu)
Очень хорошая демонстрация пользы от type-level наворотов.
The Rust language offers a promising approach to safe systems programming based on the principle of aliasing XOR mutability: a value may be either aliased or mutable, but not both at the same time. However, to implement pointer-based data structures with internal sharing, such as graphs or doubly-linked lists, we need to be able to mutate aliased state. To support such data structures, Rust provides a number of APIs that offer so-called interior mutability: the ability to mutate data via method calls on a shared reference. Unfortunately, the existing APIs sacrifice flexibility, concurrent access, and/or performance, in exchange for safety.
In this paper, we propose a new Rust API called GhostCell which avoids such sacrifices by separating permissions from data: it enables the user to safely synchronize access to a collection of data via a single permission. GhostCell repurposes an old trick from typed functional programming: branded types (as exemplified by Haskell's ST monad), which combine phantom types and rank-2 polymorphism to simulate a lightweight form of state-dependent types. We have formally proven the soundness of GhostCell by adapting and extending RustBelt, a semantic soundness proof for a representative subset of Rust, mechanized in Coq.
plv.mpi-sws.org/rustbelt/ghostcell
(thanks @dogeshibu)
#prog #amazingopensource
The Programming Languages Zoo is a collection of miniature programming languages which demonstrates various concepts and techniques used in programming language design and implementation. It is a good starting point for those who would like to implement their own programming language, or just learn how it is done.
plzoo.andrej.com
(thanks @Hirrolot)
The Programming Languages Zoo is a collection of miniature programming languages which demonstrates various concepts and techniques used in programming language design and implementation. It is a good starting point for those who would like to implement their own programming language, or just learn how it is done.
plzoo.andrej.com
(thanks @Hirrolot)
Forwarded from Backtracking (Дима Веснин)
This media is not supported in your browser
VIEW IN TELEGRAM
в чём только не делают игры! держите змейку в appkit — инструменте прототипирования интерфейсов для macos
— Полезная еда всегда почему-то самая дорогая
— Тогда почему ты не ешь манку?
— Потому что она не дорогая
— Если хочешь, могу продать её тебе задорого
#quotes #трудовыебудни
— Тогда почему ты не ешь манку?
— Потому что она не дорогая
— Если хочешь, могу продать её тебе задорого
#quotes #трудовыебудни