oxide - GitLite

KO | EN

gitlite — search

#pdf #react-native #pytorch #deep-learning #shell #reactjs #hacktoberfest #claude #tailwindcss #ui

oxide

(★ 135)

The essence of Rust.

파일 탐색기

ZIP 다운로드

- - Oxide0.v
- - level0.md
- - both-closures.md
  - rust0.md
  - rust1.md
  - rust2.md
  - rust3.md
  - rustfest-proposal.md
  - why-regions.md
- - core.rkt
  - l3.rkt
  - rust.rkt
  - rust0.rkt
- - .gitignore
  - build.sbt
- ownershipv1.md
- ownershipv2.md
- ownershipv3.md
- ownershipv4.md
- oxide0.md
- oxide1.md
- README.md
- borrowck.ml
- borrowck.mli
- borrowcktests.ml
- dune
- edsl.ml
- interp.ml
- meta.ml
- oxexe.ml
- polonius.ml
- syntax.ml
- typeck.ml
- typeck.mli
- util.ml
- - borrow_tuple_fields_2.rs
  - borrow_tuple_fields_5.rs
  - borrowck-assign-to-andmut-in-aliasable-loc.rs
  - borrowed_local_error.rs
  - kill_rules.rs
  - unnecessary_error.rs
  - unnest.rs
- - main.rs
- Cargo.lock
- Cargo.toml
- dune
- runner.ml
.ensime
.gitignore
.gitmodules
anonymizer.sh
dune-project
eval.sh
LICENSE
package.sh
README-submission.md
README.md
tests

# CDN으로 사용하기

jsDelivr

jsDelivr는 공개 GitHub 리포지토리를 별도 설정 없이 CDN으로 즉시 서빙합니다. 버전과 파일을 고르면 웹페이지에 바로 붙일 수 있는 링크와 예시 코드가 만들어집니다.

버전

파일

링크

예시

명령어 용어집

이 문서에서 사용된 명령어를 모아봤습니다. 낯선 명령어가 있다면 펼쳐서 확인해보세요.

🔍

`opam`

설명 보기 ▼

OCaml 패키지 관리자.
OCaml 컴파일러, 도구 및 라이브러리를 관리합니다.
더 많은 정보: <https://opam.ocaml.org/doc/Usage.html>.

opam init

첫 사용을 위한 opam 초기화:

opam search {{query}}

패키지 검색:

opam install {{package}}

패키지 및 모든 의존성 설치:

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

An implementation of Oxide as described in [_Oxide: The Essence of Rust_][arxiv].

## Background

To get a sense of the terminology and why the semantics is structured how it is (i.e. into levels),
I highly recommend reading [Niko's post about observational equivalence in Rust][obseq]. This should
at least be sufficient to understand why we're talking about levels of Rust, but it may well provide
other useful insights as well. [Niko's recent work on non-lexical lifetimes][nll] features some key
similarities to our approach, and may aid in its understanding.

## Terminology

- _Safe Rust_ — the core of Rust, without _any_ unsafe code.
- _Language level_ — a combination of _safe Rust_ and a set of _unsafe abstractions_ that increase
  the overall expressivity of the language, e.g. Rust1 is _safe Rust_ + `Vec<T>`.
- _Unsafe abstraction_ — an abstraction that cannot be implemented in _safe Rust_ (absolute) or the
  current _language level_ (relative) without the use of Rust's `unsafe` block.
- _Lifetime_ — the span of time from when a value is allocated to when it is deallocated.
- _Region_ — the space on the stack where a value is allocated for its _lifetime_ (see also:
  [`why-regions.md`](notes/why-regions.md)).

## Navigating this repository

This repository is split into six parts:

1. [`history/`](history/) — largely-iterative prior attempts at building & designing Oxide
    - [`ownershipv1`](history/ownershipv1.md) and [`ownershipv2`](history/ownershipv2.md) both have
      some notes included that might be insightful to some degree. Evidently, I got lazy afterward
      and stopped writing actual prose in the models. Afterward, I switched to LaTeX.
2. [`history/notes/`](history/notes/) — an assorted selection of my old notes
3. [`history/examples/`](history/examples/) — a collection of old examples (and counter-examples) at each level
    - Each example is in "proper" Rust syntax for that level _and_ its corresponding `oxide` form at the time.
4. [`oxide/`](oxide/) — an implementation of Oxide in OCaml
    - Currently, it's just the type checker, but we will eventually have an interpreter too.
    - We require OCaml 4.08 for user-defined binding form support.
5. [`reducer/`](reducer/) — a desugarer (simple compiler) from (a subset of) Rust to Oxide
    - Run reducer with `RUSTFLAGS='--cfg procmacro2_semver_exempt'` for source filename tracking.
6. [`runner/`](runner/) — a test harness for driving the reducer/typechecker. 
    - This requires the following opam packages:
    `opam install opam shexp stdio yojson utop ppx_deriving`

## Related Works

- [Linear Regions Are All You Need][linrgn]
- [L3: A Linear Language with Locations][linloc]
- [A Step-Indexed Model of Substructural State][substruct]
- [Checking Interference with Fractional Permissions][fracperm] ([[No Paywall]][fracperm-cc])

[arxiv]: https://arxiv.org/abs/1903.00982
[obseq]: http://smallcultfollowing.com/babysteps/blog/2016/10/02/observational-equivalence-and-unsafe-code/
[nll]: http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/
[linrgn]: http://www.ccs.neu.edu/home/amal/papers/linrgn.pdf
[linloc]: http://www.ccs.neu.edu/home/amal/papers/linloc-techrpt.pdf
[substruct]: http://www.ccs.neu.edu/home/amal/papers/substruct.pdf
[fracperm]: https://link.springer.com/content/pdf/10.1007%2F3-540-44898-5_4.pdf
[fracperm-cc]: https://commie.club/papers/boyland03:frac-permissions.pdf