magmide / magmide Goto Github PK

Hello,

While reading a comparison of this project goals with other existing languages I was somewhat appalled by a misjudgement about Lean in particular, which I'm happened to be familiar with. Believe me, that comparison missed target on most points: Lean is not developed in academy, it's targeted for practical software development by Microsoft, it is developed by engineers and for engineers as well, it's not interpreted language, also its metaprogramming model was partially inspired by Racket and Rust if that matters. AFAIK there are even plans to support Iris in the future. But it's true that Lean is a pure functional programming language (like Haskell), though it does have some innovative "imperative"-like constructs and optimizations. Also, it's true that Lean 4 is in early development stages and it is still mostly adopted for formalizing mathematics at the moment.

Of course, don' trust my words on this, I'm not an expert myself. But to avoid poor judgement and probably before wasting some of your efforts, I would sincerely suggest to ask opinion of Lean developers and experts in these matters, e.g. https://leanprover.zulipchat.com I'm sure they will be happy to discuss it with you. Please, bear in mind that Lean 3 (stable version) and Lean 4 are quite different and incompatible languages! Also mathlib is not Lean and they should not be confused!

If you truly want to make this a practical language, you're going to accept knots in your turing tape. That is, if you assume all addressable memory is just an ordinary read/write cell, you'll have left out the richness (and weirdness) of memory. Off the top of my head:

• Thread local storage
• Memory mapped I/O
• Memory mapping in general (IIRC, it's possible to tie a knot in memory; that is, map two virtual addresses to the same physical memory, so writing one range changes the other range, all within the same process)
• Read-only memory
• Write-only memory
• Pretty much anything involving GPU memory
• Memory alignment (if you want to do any systems programming, this will be an issue)

I suspect that means that you'll need a mechanism to not only describe attributes of a memory range, you'll need the mechanism to be able to operate over time. Rust has dipped its toe into this, with the whole lifetimes syntax, but I suspect that is just the start. For example, can you put dates and durations into the language? If I have a CPU and a GPU, each of them running at slightly different clock rates, there needs to be some method of making them communicate (e.g., PCI, etc.) that can handle the mismatch.

These are literally off the top of my head, there may be other issues as well, I just wanted to make certain that you can deal with them within Magmide.

the readme is long af and the more i look at the source code the more confused i get.. ehh can someone explain it to me?

Recently I found your project and was very surprised how clearly it describes the ideas that I recently came up with about my programming language. Therefore, I really want to discuss the project with you and take part in its development. I sent you an email with links to my accounts.

B-Method, like magma, aimed at correct code generation and was successfully used in several projects, as was the follow-on project the Rodin tool.

I was involved in the development of a transactional logger using the B-Method. The implementation was sound, but the generated code was massively bloated and had to be hand-ported to produce a more compact implementation.

You may like to compare notes with this approach.

ATS is a kinda a scary language. How your project differs from this proof writing language. This language tops the programming benchmark chart until it was removed because there isn't enough experts in the language

https://www.youtube.com/watch?v=zt0OQb1DBko

https://github.com/githwxi/ATS-Xanadu

https://github.com/magmide/magmide/blob/main/posts/comparisons-with-other-projects.md

https://stackoverflow.com/questions/26958969/why-was-the-ats-language-dropped-from-the-computer-language-benchmarks-game

https://ats-lang.github.io/DOCUMENT/INT2PROGINATS/PDF/main.pdf

Can you evaluate the language?

I personally have never written hello world in this language.

Hi,

I don't usually like to pick on names, but I often use a different, much older, mathematics related language, magma: https://en.m.wikipedia.org/wiki/Magma_(computer_algebra_system)

I just wanted to check you were aware of it, as I expect if your system gets popular, there will be confusion (in both directions).

Hi! I like the ideas in the posts you've published here.

As I've been reading I've had some thoughts or questions pop up, but it felt off to open an issue about it because issues carry some additional baggage such as the expectation of a response, the implication that it requires some action, and the decision to close, none of which would align with my intent to simply comment. I've observed this mismatch in other issues as well.

Perhaps such commentary would be better packaged by Discussions. What do you think about enabling the Discussions repository feature? Or more generally, do you have plans for building a community around magmide? (chat, forums, meetups, etc)

I wonder whether you could make some use of the (IMHO mind-blowing in a sense) language Basil (some cool features) as it offers "compile-time first" approach to writing apps because its syntax is the very same thing in compile-time as in runtime with zero differences.

Basil is thus not a "new level" of metaprogramming, but the "highest possible level" of metaprogramming. This has serious implications for just about anything and especially safety - because my incentive is to leverage the full power to create safety primitives tailorable to every imaginable use case (pretty much how you describe in your readme the "level of safety" required when importing libs or reusing existing code on new places).

Thoughts?

I've spent a good amount of time thinking about how the world would be changed by more reliable software and how I wish more languages tried to push the frontier instead of just picking new points on the Pareto curve. Rust's attempt to get improved safety without performance sacrifices is the best recent example of a language both doing this and aiming for mainstream acceptance. Magmide looks like it's trying to do that on steroids, so there is a lot in the README for me to agree with and get excited about even if there's nothing concrete yet.

However, as you pointed out research debt makes a lot of this inaccessible. How would you suggest people with similar goals or would-be contributors get up to speed? This is assuming people in the target audience for the final product: experienced imperative programmers without any familiarity with the advances in the academic world, so no knowledge of Coq/Agda/Iris/dependent-types/formal-logic etc. Since it's a goal to make something they would find accessible it seems like figuring out how to inform possible contributors could overlap with figuring out how to make the language more easily learnable.

Github Discussions and Issues are a good way to coordinate contributors and manage code development. However I think it would be nice to have a Discord server or a Telegram chat to talk about language design topics like type theory, software verification, programming patterns and other general ideas not directly related to code and implementation. Is there anything similar to that?

I'm just a curious onlooker in the field of formal verification of software (basically purely by virtue of having subscribed to Hillel Wayne's newsletter), so most of the README is way above my paygrade. However, even with my very superficial knowledge, I was expecting a comparison with TLA+ (see also https://www.learntla.com/), which has already been adopted by some parts of the industry where correctness is critical or can save a lot of money.

Since Magma also has the ambition to improve real-world software projects, a comparison with TLA+ would be helpful. What does Magma plan to bring to the table that TLA+ doesn't offer? Does it have a broader scope that encompasses TLA+'s and adds more? Or would they essentially be complementary tools?

As the title states, the link https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf results in a 404

Some 30 years ago, I worked on introducing formal verification into an existing software project. The project failed, as described in this paper, essentially because asking programmers to do the necessary proofs by hand was unrealistic. At least one other attempt was made to take a similar approach and reduce the amount of proof required. Both these projects built on "Cleanroom software engineering" which aims to refine specifications to a subset of an existing programming language. The subset is chosen such that proof rules can be written for each language construct in the subset.

Adopting a similar approach for magma could help to get the project bootstrapped. If a suitable language and subset can be identified and proof rules written, there would be no need to develop a compiler before making progress on other aspects of magma. Without some incremental approach like this, I fear the scope of magma and the set of skills required to get it going will turn out to be overwhelming. With a suitable choice of language (e.g. Rust) it may even be possible to generate more interest in magma and thereby gain traction.

But regardless of how you proceed, I wish you every success.

Frama C is a project aimed at formally verified C code. With its weakest precondition calculus, it's possible to state assertions about C code that can be formally checked.

Since you're attempting to make a formally verified systems programming language, I'm curious what are your thoughts on it, since that's exactly what it does.

Love this idea! I think the vision is truly compelling and worth the bet. Coming from the Web3 industry, I believe this project can play a big role in making more secure smart contracts, and I believe a good audience to target as early adopters. Also there’s money there, and a strong culture of funding public goods.

Can you please add a donate button so that people can help out even if they don’t have time? Also, I think this could be a great project for https://gitcoin.co/grants/.

Hi, this is very interesting project!
I've just found these small "typos" in intro-verification-logic-in-magmide.md:

1. // standard signed and unsigned integers
   let unsigned_8_bits: u8 = 0    // should be `let signed_8_bits: i8 = 0`
   let unsigned_8_bits: u8 = 0
   

   (src)

2. alias Range; i32, i32 & > ^.1    // should be  `alias Range; i32, i32 & > ^.0`
   

   (src)

Can I create a PR?