💾 Archived View for dioskouroi.xyz › thread › 29360663 captured on 2021-11-30 at 20:18:30. Gemini links have been rewritten to link to archived content

-=-=-=-=-=-=-

Magma: A Dependently-Typed Language

Author: todsacerdoti

Score: 40

Comments: 8

Date: 2021-11-27 15:03:36

Web Link

________________________________________________________________________________

vzaliva wrote at 2021-11-27 16:41:06:

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.

dandotway wrote at 2021-11-27 20:40:19:

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.

new_stranger wrote at 2021-11-27 19:30:26:

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.

klyrs wrote at 2021-11-27 17:10:21:

Not to be confused with Magma the computer algebra system

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

milleramp wrote at 2021-11-27 23:42:14:

Or the French rock band founded in 1969:

https://www.magmamusic.org/en/home/

thesuperbigfrog wrote at 2021-11-28 04:05:13:

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

dandotway wrote at 2021-11-28 07:28:02:

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

xiaodai wrote at 2021-11-28 09:22:15:

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