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 →
Magmide Alternatives
Similar projects and alternatives to magmide
-
-
SonarLint
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.
-
tectonic
A modernized, complete, self-contained TeX/LaTeX engine, powered by XeTeX and TeXLive.
-
-
practical-fm
A gently curated list of companies using verification formal methods in industry
-
-
-
InfluxDB
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.
-
prusti-dev
A static verifier for Rust, based on the Viper verification infrastructure.
-
-
electrolysis
Simple verification of Rust programs via functional purification in Lean 2(!)
-
flexbugs
A community-curated list of flexbox issues and cross-browser workarounds for them.
-
.NET Runtime
.NET is a cross-platform runtime for cloud, mobile, desktop, and IoT apps.
-
-
-
rust-verification-tools
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
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" [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
-
A note from our sponsor - SonarLint
www.sonarlint.org | 25 Mar 2023