[HN Gopher] Magma: A Dependently-Typed Language
___________________________________________________________________
Magma: A Dependently-Typed Language
Author : todsacerdoti
Score : 30 points
Date : 2021-11-27 15:03 UTC (7 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| klyrs wrote:
| Not to be confused with Magma the computer algebra system
|
| http://magma.maths.usyd.edu.au
| vzaliva wrote:
| 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:
| 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:
| 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.
___________________________________________________________________
(page generated 2021-11-27 23:01 UTC)