magmide
fleet
Our great sponsors
magmide | fleet | |
---|---|---|
22 | 17 | |
803 | 2,413 | |
0.9% | 0.5% | |
6.9 | 2.9 | |
16 days ago | 10 months ago | |
Coq | Rust | |
- | Apache License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
magmide
-
Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think?
https://github.com/magmide/magmide when
-
Kani 0.29.0 has been released!
How close are we to this https://github.com/magmide/magmide
-
Make formal verification and provably correct software practical and mainstream
I really want to like this, but it really comes across as more of a wishful thinking project without a lot of experience or intuition about how to solve the very real problems that formal methods run into in this domain. Like, the design goals literally include "verify any program" [1], which is almost certainly impossible.
Important questions like how you implement the design pillars without running smack into the issue of decidability seem entirely ignored. They have a whole section on how "this idea exists in an incentive no man's land" without seemingly being aware of the rich history of formal methods in low level programming, from Ada through Java through formal C through Rust itself. The common issues these encountered like decidability, holes in the formal model (which contributed to the downfall of the Java sandbox as a security boundary), and the combinatorial explosion inherent in verification tools are all huge looming questions that should at least be mentioned.
Maybe I'm being overly critical here, but it all makes me wonder whether the project is even possible.
[1] https://github.com/magmide/magmide/blob/main/posts/design-of...
-
Hello Letlang! My programming language targeting Rust
I would love to play around with a compiled language with as powerful a compile-time type system/proof assistant as Lean or Coq. I saw some early work in the Rust realm here: https://github.com/magmide/magmide
- Software can literally be perfect (talks about some important logical ideas that make the Rust ownership system work, and how we could build a provably correct Rust compiler)
-
My Path to Magma
The Magma name requires disambiguation:
His Magma programming language: https://github.com/blainehansen/magma
> The goal of this project is to: create a programming language and surrounding education/tooling ecosystem capable of making formal verification and provably correct software mainstream and normal among working software engineers.
Magma computer algebra system: https://en.wikipedia.org/wiki/Magma_(computer_algebra_system...
> Magma is a computer algebra system designed to solve problems in algebra, number theory, geometry and combinatorics. It is named after the algebraic structure magma. It runs on Unix-like operating systems, as well as Windows.
-
Magma, a project I hope will make provably correct software possible for everyone
The current design thinking is spelled out in the repo: https://github.com/blainehansen/magma
The idea with notations isn't to make custom symbology impossible, just clearly signaled, much in the same way Rust macros can do whatever they want but have to be underneath some macro_name!esque indicator. Check out my rough design thoughts for more if you're interested :) https://github.com/blainehansen/magma/blob/main/posts/design-of-magma.md
fleet
-
Help me love Rust - compilation time
fleet is an awesome tool for faster builds for non-production purposes. In some cases it gave me 10-15x compilation speed.
-
why rust compiler is slow?
one simple way is to use fleet, they have collected most of optimizations possible for building.
-
Welcome to the Reddit!
Hey there! I’m Grinder, the community manager of Dimension. Dimension is an awesome project that has published a ton of useful open source projects, such as fleet and volt. You can view our Github for all our projects that we’ve released.
-
Welcome to the Reddit Community!
We’ve created awesome things, such as fleet and volt.
-
Hello Letlang! My programming language targeting Rust
Since each Letlang module compiles to a single crate, crates are very small and their build can be parallelized quite easily (see https://github.com/dimensionhq/fleet). My hypothesis is that this will help reduce build time.
- Sccache – Shared Compilation Cache
- fleet - The blazing fast build tool for Rust.
-
Show HN: Experimental] Fleet – A build tool for Rust that's upto 5x faster
Fleet is an experimental fast, lightweight, open-source, build tool for Rust.
Builds with Fleet enabled are up-to 5x faster!
For a production repository (infinyon/fluvio) which we tested, we were able to cut down our incremental build times from 29 seconds down to 9 seconds, boosted by Fleet. We saw even better results on dimensionhq/volt, with our build times cut down from 3 minutes to just 1 minute - a 3x speed improvement!
How does fleet work?
Fleet works by optimizing your builds using existing tooling available in the Rust ecosystem, including seamlessly integrating sccache, lld, zld, ramdisks (for those using WSL or HDD's) et al.
You can get fleet at the official website.
Check out fleet over at https://github.com/dimensionhq/fleet and our website at https://fleet.rs
Looking forward to your feedback and thoughts!
-
[experimental] Fleet - A build tool for Rust that's upto 5x faster!
It turns out fleet-rs is in https://crates.io, I'll just check https://github.com/dimensionhq/fleet directly
The best part? Fleet is open source - https://github.com/dimensionhq/fleet! If you would like to support Fleet development or find the project interesting, a ⭐ would be hugely appreciated!
What are some alternatives?
Rudra - Rust Memory Safety & Undefined Behavior Detection
line-combination-proofs
tectonic - A modernized, complete, self-contained TeX/LaTeX engine, powered by XeTeX and TeXLive.
z3 - The Z3 Theorem Prover
practical-fm - A gently curated list of companies using verification formal methods in industry
fluvio - Lean and mean distributed stream processing system written in rust and web assembly.
prusti-dev - A static verifier for Rust, based on the Viper verification infrastructure.
volt - An experimental package management tool for JavaScript. Upto 30x faster installation of dependencies using pre-flattened dependency trees.
mold - Mold: A Modern Linker 🦠
csharplang - The official repo for the design of the C# programming language
electrolysis - Simple verification of Rust programs via functional purification in Lean 2(!)
fiat - Mostly Automated Synthesis of Correct-by-Construction Programs