Thoughts (if you *truly* wish to make this a practical language) about magmide HOT 4 CLOSED

I'm sorry!!! 🙇‍♂️ I didn't mean any offense at all! I had NO intention of being rude towards you, I actually love what you're trying to do with the project! I was concerned about the memory models situation because I've seen too many languages not think about this aspect, and the result is... less than useful. I'll try to be less sharp in the future.

from magmide.

It's my fault; I have a tendency to be quite abrupt in my speech and writing style, which has been an issue for me my whole life. I normally re-read messages several times before I send them in an effort to avoid my normal lack of tact, but your project got me pretty excited, and I just kind of... did what I usually do. Again, my apologies for offending you!

from magmide.

Awesome thank you for being nice :) We all accidentally come in too hot sometimes ha, I certainly do :) I was maybe being too sensitive ha but thanks for being considerate

from magmide.

I agree it's absolutely necessary for a memory model to be as accurate as possible! Not all projects need to concern themselves with this level of detail though. It's important to point out the Magmide design isn't really a "normal" language that most of us are used to dealing with. The logical dependently typed pure functional part is really the place where the power of the language rests. That logical component would be capable of defining any logical model you want (you can already define any logical model you're capable of in languages like Coq, it's just really difficult to use those models to metaprogrammatically assemble real code).

So yes all of these things are possible (you should read about separation logic and the "Iris from the ground up" paper to understand how even things like time-dependent memory requirements or access modes that can be changed by one process but not by others are all possible to model), and lower level code like operating systems would likely want to fully deal with all this complexity in order to provide higher level systems with verified abstractions.

I appreciate you bringing these thorny questions up :) I do however want to let you know that the way you've done so is kinda sharp and flippant and bordering on rude ha. I'll absolutely remember these points though!

from magmide.