-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Xavier Denis
authored and
Xavier Denis
committed
Sep 5, 2024
1 parent
f9cc8a0
commit b49f5c5
Showing
14 changed files
with
163 additions
and
261 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,10 +1,41 @@ | ||
name: Deploy mdBook | ||
env: | ||
cache_generation: 2024-03-04 | ||
|
||
name: Deploy site | ||
|
||
on: [push] | ||
|
||
jobs: | ||
build: | ||
runs-on: ubuntu-latest | ||
env: | ||
ZOLA_VERSION: 0.16.0 | ||
steps: | ||
- uses: actions/checkout@v2 | ||
- uses: XAMPPRocky/[email protected] | ||
with: | ||
token: ${{ secrets.GITHUB_TOKEN }} | ||
- uses: actions/checkout@v3 | ||
- name: Install Zola | ||
run: | | ||
curl -sL https://github.com/getzola/zola/releases/download/v${ZOLA_VERSION}/zola-v${ZOLA_VERSION}-x86_64-unknown-linux-gnu.tar.gz | tar xz -C /usr/local/bin | ||
- name: Build with Zola | ||
run: | | ||
zola build --drafts | ||
zola build | ||
- name: Upload artifact | ||
uses: actions/upload-pages-artifact@v3 | ||
with: | ||
path: ./public | ||
deploy: | ||
needs: build | ||
|
||
permissions: | ||
pages: write | ||
id-token: write | ||
|
||
environment: | ||
name: github-pages | ||
url: ${{ steps.deployment.outputs.page_url }} | ||
|
||
runs-on: ubuntu-latest | ||
steps: | ||
- name: Deploy to GitHub Pages | ||
id: deployment | ||
uses: actions/deploy-pages@v4 # or specific "vX.X.X" version tag for this action |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
# The URL the site will be built for | ||
base_url = "https://rust-formal-methods.github.io" | ||
|
||
# Whether to automatically compile all Sass files in the sass directory | ||
compile_sass = true | ||
|
||
# Whether to build a search index to be used later on by a JavaScript library | ||
build_search_index = false | ||
|
||
theme = "anemone" | ||
|
||
title = "Rust Formal Methods Interest Group" | ||
|
||
[markdown] | ||
# Whether to do syntax highlighting | ||
# Theme can be customised by setting the `highlight_theme` variable to a theme supported by Zola | ||
highlight_code = true | ||
|
||
[extra] | ||
# Put all your custom variables here |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
+++ | ||
title = "RFMIG meetings" | ||
+++ | ||
meetings section |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,29 @@ | ||
+++ | ||
title = "Contracts in Rust" | ||
date = 2024-09-24 | ||
+++ | ||
**Title**: | ||
|
||
**Abstract**: | ||
|
||
As the growing number of verification tools (Aeneas, Creusot, Kani, Prusti, Verus, ...) has shown, there is a growing community for formal verification of Rust code. | ||
Each of these tools needs to re-invent a specification language, leading to a rapidly fragmenting ecosystem of incompatible languages and tools. | ||
To address this and related challenges, a Major Change Proposal was proposed to integrate support for contracts and invariants into Rust. | ||
But what does this mean? | ||
|
||
Today, current tools must either embed a whole additional specification language via macros, or attemt to parse contracts from `assert!` and related features. | ||
Both solutions leave a lot to be desired, as this makes it difficult for users to use these tools, while also hindering the development of said tools. | ||
It also means that each tool has its own language, making interoperability hard. | ||
|
||
The shiny future we are aiming for is one in which ordinary Rust programmers are writing contracts as part of every day Rust to be verified with dynamic (and static) tools. | ||
Rather than building their codebase around a single verifier, they can just "plug in" different verifiers, reusing the majority of their contracts. | ||
|
||
In this talk we present a vision for how we might get to this future, and some of the steps we can take on the way there. | ||
|
||
**Presenter**: | ||
|
||
Felix has been working on the Rust compiler since before Rust 1.0; he was co-lead of the Rust compiler team from 2019 until 2023. Felix has taken on this work as part of a broader interest in enforcing safety and correctness properties for Rust code. | ||
|
||
**Meeting Link**: | ||
|
||
**Recording Link**: |
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
Binary file not shown.
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.