-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
creusot
Discontinued Creusot helps you prove your code is correct in an automated fashion. [Moved to: https://github.com/creusot-rs/creusot] (by xldenis)
-
rust-verification-tools
Discontinued RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
-
misra-rust
An investigation into what adhering to each MISRA-C rule looks like in Rust. The intention is to decipher how much we "get for free" from the Rust compiler.
-
advent_of_code
This repository contains solutions to Advent of Code challenges (by joakim-strandberg)
-
-
sdlada
Ada 2022 bindings to SDL 2 - Don't STAR this, this is my personal repo which I may delete over using the AGF one.
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
Ferrous's embedded Rust tooling is outstanding. Ie its [Knurling App template](https://github.com/knurling-rs/app-template), and associated Probe-run, Deft, and flip-link.
These make flashing and debugging Rust embedded very easy - easier than any embedded toolchain I've seen besides Arduino.
This is exciting! I've met with people from AdaCore and Ferrous systems (individually) several times and they're all serious, competent and motivated.
I'm curious what kinds of software they want to (eventually) verify, my PhD thesis is developing a verification tool for Rust (https://github.com/xldenis/creusot) and I'm always on the look out for case studies to push me forward.
The road to formally verified Rust is still long but in my unbiased opinion looking quite bright, especially compared to other languages like C.
There's rubble.
https://github.com/jonas-schievink/rubble
We've been approached by multiple parties to finish it and we are up to it, but the final effort, particularly certification is currently prohibitive. Serious inquiries taken, though - we're also happy to play "consortium" in that this does not have to be financed by any single party.
I hope someone also picks up the work started in https://project-oak.github.io/rust-verification-tools/ - the idea of having a `cargo verify` tool that supports different backends is great for bridging the academic PoCs with something that an average programmer can integrate into the dev workflow.
I already do, my tool produces WhyML modules from Rust crates. But we can leverage Rust's ownership typing to drastically reduce proof obligations related to pointers and memory.
Incidentally, I've started working on a VSCode frontend to Why3 to replace the existing GTK one (https://github.com/xldenis/whycode), I'm currently rewriting the PoC as an LSP extension.
Rust makes quite a few things more rigorous (e.g. pairing allocations with deallocations and reference validity). It basically fulfills the job of a static analyzer baked into the language.
It's also a vastly more analyzable language (in that its syntax is reasonably unambiguous and there's no dynamic runtime in play) and it can be integrated well.
Toolchain quality (error reporting, built in testing, awareness of primitives like "libraries", etc.) is also a huge strong point.
We're reasonably confident that we can use safe Rust as is, with strong guidance on how to do unsafe Rust.
For a tangible investigation of that space, PolySync has a project that has a look at MISRA rules from a Rust perspective. https://github.com/PolySync/misra-rust/blob/master/MISRA-Rul...
Ada is a good example here: the language has not evolved something like MISRA-C (it has evolved SPARK for formal verification, but I see that differently).
It's kind of the opposite for me. It takes much less time to understand what Ada-written code is doing compared to any of the C-type languages, or even Rust. It is very plainly written. Verbose, yes, but much more plainly written.
Just take a look at this, and tell me it's not legible: https://github.com/joakim-strandberg/advent_of_code/blob/mas...
It is an April Fools Day joke. They forked GCC 10 and made one commit on April Fools Day 2021, and haven't touched it sense.
Compare:
Ada++ -- https://github.com/AdaPlusPlus/gcc/commits/master
GCC 10 (history from April 2021) -- https://github.com/gcc-mirror/gcc/commits/releases/gcc-10?af...
You can use any version of gnat to build [this](https://github.com/Lucretia/sdlada)
Feel free to reach out, it's a topic of interest to us. A good place to discuss is for example the AeroRust Discord or just send me an email. https://github.com/AeroRust/Welcome