magmide VS rust-verification-tools

https://github.com/magmide/magmide when

How close are we to this https://github.com/magmide/magmide

https://github.com/magmide/magmide#isnt-most-software-too-fu...

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...

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

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.

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

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.