Unsafe, Miri, SIMD - June Meetup

Unsafe Rust and Miri by Ralf Jung (https://ralfj.de/blog/):
Memory safety is one of the key selling points of Rust. However, even the Rust compiler is not omniscient, so sometimes programmers need to resort to "unsafe" code and take on the responsibility of ensuring memory safety themselves. In this talk I will introduce key terms surrounding unsafe code such as "undefined behavior" and "soundness", and explain how to write unsafe code in a systematic way that reduces the chance of getting it wrong. I will also demonstrate how you can use Miri to check your unsafe code for otherwise hard-to-detect bugs.

SIMD instructions with Rust on Android by Guillaume Endignoux (https://github.com/gendx):
SIMD instructions have become increasingly important to speed up algorithms, and Rust now exposes them as intrinsics in the standard library.
However, SIMD presents unique challenges, among others: portability, testability, usability, and making sure the compiler indeed generated optimized code.
In this talk, I'll take the angle of using Rust on Android to discuss how to approach and solve these challenges.

Verus - Verified Rust for low-level systems code by Andrea Lattuada (https://andrea.lattuada.me/):
Rust programmers care about the correctness of their code and, while the Rust type system and its memory safety are excellent foundations, they aren’t sufficient to ensure correctness. “Full functional verification" of code is an alternative (or a complement) to tests that uses formal methods to prove that the behaviour of a complex program corresponds to a desired specification, i.e. to prove that the program is "correct".

We are building our new tool, Verus, to efficiently verify full functional correctness of low-level systems code written in a safe Rust dialect that supports expressing specifications and proofs. In this talk I'll introduce the basics of functional verification, the verification technique used by Verus, and I'll demonstrate how the tool, with the programmer's help, can ensure that programs are bug-free (or how it catches bugs, if they are any).

Timetable:
All talks are roughly 30min with 10min Q&A at the end and a 5min breather for a laptop change.

• 18:00 doors open
• 18:15 Talk 1
• 19:00 Talk 2
• 19:45 Talk 3
• 20:30 Socialising maybe in a different location

We are looking for more speakers:
Who will it be? What will the topic be? If you want to submit your guess or proposal, write us in our Matrix room:
https://matrix.to/#/#rust-zuerisee:matrix.coredump.ch or on any other channel listed here:
https://estada.ch/support-my-work/