diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml index 0160f8f..56ac037 100644 --- a/.github/workflows/book.yml +++ b/.github/workflows/book.yml @@ -5,6 +5,7 @@ name: Deploy site on: push: + pull_request: schedule: - cron: '0 2 * * *' @@ -29,6 +30,7 @@ jobs: with: path: ./public deploy: + if: startsWith(github.repository, 'rust-formal-methods/') && github.event_name != 'pull_request' needs: build permissions: @@ -43,4 +45,4 @@ jobs: steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v4 # or specific "vX.X.X" version tag for this action \ No newline at end of file + uses: actions/deploy-pages@v4 # or specific "vX.X.X" version tag for this action diff --git a/content/meetings/verifast-rust.md b/content/meetings/verifast-rust.md index b042000..f847bec 100644 --- a/content/meetings/verifast-rust.md +++ b/content/meetings/verifast-rust.md @@ -1,6 +1,6 @@ +++ title = "Towards Sound `unsafe` Rust" -date = 2024-10-28T19:00:00+01:00 (Paris/Zurich) +date = 2024-10-28T19:00:00+01:00 # (Paris/Zurich) +++ Rust guarantees memory safety and data race freedom through its type checker, which enforces *ownership* and *borrowing* rules. However, adhering strictly to these rules can limit expressiveness and restrict certain high-performance implementations. To address this limitation, Rust allows programmers to relax some type system checks within `unsafe` blocks. The challenge, however, is that maintaining type system invariants within these relaxed blocks becomes the programmer's responsibility.