My Path to Magma | Hacker News Reader

My Path to Magma

blainehansen.me

The Magma name appears to require 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.

I was just about to post the same thing. I don't like picking on things like names, but the "old magma" is still very popular in mathematics.

I heard from a friend (have not verified myself) that the paper in which the Magma computer algebra system was introduced is the most-cited paper in the whole of pure mathematics.

There is a discussion about how to define this and a comment concluding that indeed by one metric the Magma paper is most cited here: https://mathoverflow.net/questions/199978/the-most-cited-pap...

John Cannon, who started Magma, pushed very hard for people to cite that paper whenever they used Magma in a paper. We eventually did something similar with SageMath for a bit, but it felt weird having everybody cite a paper with me personally as the main author, when there are nearly 1000 contributors to Sage, so we made up a reference with the author “The Sage Developers”, or something like that. As a result there is probably no MathSciNet entry tracking citations to Sagemath even though many papers cite Sagemath.

My first thought was the Magma object database https://github.com/magma-database/magma

And here I was hoping someone was deep diving the prog rock rabbit-hole:

https://en.wikipedia.org/wiki/Magma_(band)

Does this offer any advantages to Ada/Spark? Having worked in formal method environments there's a lot to be said of a tool that's been around for a while. Even with formal methods you can still have bugs and there's a risk in using new tools. Without getting those millions of hours of development time it's hard to know a tool really works regardless of the theory behind it.

Yeah, he talks as if this hasn't been tried before. See agda or Idris.

I like this idea. I hope to use the language someday and translate (upgrade) my Rust code to it.

Reply on news.ycombinator.com