Magma: A Dependently-Typed Language | Hacker News Reader

Magma: A Dependently-Typed Language

github.com

42 pointstodsacerdoti8 comments

I know negative comments are frowned upon here, but I can't help pointing out that there is no language to talk about yet. Following this link, one will discover many notes and thoughts written by somebody who seems enthusiastic, passionate, and a little naive in my opinion about dependent types and formal verification. I wish him luck and will be curious to see what may come from this, but the results are probably years from now.

The boxer Mike Tyson put it well, "Everyone has a plan until they get punched in the mouth."

I discovered Coq and OCaml by way of the Frama-C framework for formally verifying C programs. This is a system that works today. It does need to be made lower friction to install and get started with, but the author of this repo bashes on Coq and its researchers as if he were a young firebrand politician taking on Big Tobacco and Big Pharma. He even says, 'And let's be honest, the name "Coq" is just terrible.'

I wish him well on his crusade against Big Coq.

I love all the to-the-point "why?" questions. There are many other problems (like no actual product) with this repo, but hammering out all the tough answers upfront is a breath of fresh air.

I've visited over 4,000 github projects and my first question "what? why?" is often harder than it should be to answer from the readme and source.

Not to be confused with Magma the computer algebra system

http://magma.maths.usyd.edu.au

Or the French rock band founded in 1969: https://www.magmamusic.org/en/home/

SPARK is a real-world system that allows some degree of formal proofs in the programming language and related tools:

https://learn.adacore.com/courses/intro-to-spark/index.html

https://docs.adacore.com/spark2014-docs/html/lrm/introductio...

I've tried SPARK. Compared to Frama-C, SPARK is not as powerful. Frama-C can prove the correctness of arbitrary heap manipulation algorithms. SPARK can handle singly linked lists but not doubly linked lists (last I checked).

Although, usually the people who use SPARK use it because it is certified for their industry (such as aerospace).

This is the 2nd programming language called Magma! University of Sydney has one for pure math.

Reply on news.ycombinator.com