Magmide

Stream: general

[Arthur Paulino]

Has anyone seen Magmide?
This file shows their main design goals, apparently

[Jannis Limperg]

I looked at it a few weeks ago when it was posted on Reddit. The vision looked okay, but imo the project is hilariously overscoped. They want to create not just a dependently typed language with fancy metaprogramming but also an imperative object language and a program logic for it. It's just a lot, especially since the guy behind it doesn't seem to be an expert in any of these domains. So while I wish him luck, I wouldn't hold my breath.

[Violeta Hernández]

As someone who's worked on overambitious projects with little technical knowledge... man, I just wish them well

[Mario Carneiro]

Wow, this is very close in design goals to MM0 / Metamath C. I'm with Jannis in that I'll hold off judgment until I actually see more than a tech startup pitch. (Obviously I'm very on board with the pitch.)

[Mario Carneiro]

...oh right, I had a conversation with the author about magmide back in November. He's clearly better at marketing than me based on the github stars, although I'm not brave enough to start marketing MM0 to general programmers yet