Up your coding game and discover issues early. SonarLint is a free plugin that helps you find & fix bugs and security issues from the moment you start writing code. Install from your favorite IDE marketplace today. Learn more →
Similar projects and alternatives to magmide
Rust Memory Safety & Undefined Behavior Detection
Clean code begins in your IDE with SonarLint. Up your coding game and discover issues early. SonarLint is a free plugin that helps you find & fix bugs and security issues from the moment you start writing code. Install from your favorite IDE marketplace today.
A modernized, complete, self-contained TeX/LaTeX engine, powered by XeTeX and TeXLive.
The Z3 Theorem Prover
A gently curated list of companies using verification formal methods in industry
Mostly Automated Synthesis of Correct-by-Construction Programs
Dafny is a verification-aware programming language
Access the most powerful time series database as a service. Ingest, store, & analyze all types of time series data in a fully-managed, purpose-built database. Keep data forever with low-cost storage and superior data compression.
A static verifier for Rust, based on the Viper verification infrastructure.
The official repo for the design of the C# programming language
Simple verification of Rust programs via functional purification in Lean 2(!)
A community-curated list of flexbox issues and cross-browser workarounds for them.
.NET is a cross-platform runtime for cloud, mobile, desktop, and IoT apps.
The seL4 microkernel
🚀 The blazing fast build tool for Rust. (by dimensionhq)
RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.
Multi-user object database (by magma-database)
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
magmide reviews and mentions
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" , 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.
Hello Letlang! My programming language targeting Rust
2 projects | reddit.com/r/rust | 14 May 2022
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)
2 projects | reddit.com/r/rust | 16 Feb 2022
My Path to Magma
2 projects | news.ycombinator.com | 4 Dec 2021
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
9 projects | reddit.com/r/rust | 18 Nov 2021
The current design thinking is spelled out in the repo: https://github.com/blainehansen/magma9 projects | reddit.com/r/rust | 18 Nov 2021
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
A note from our sponsor - SonarLint
www.sonarlint.org | 25 Mar 2023