Build magma on a subset of an existing language

[magmide]

Build magma on a subset of an existing language

[glyn]

That's gracious of you. Please skip my paper as it's behind a paywall and you won't learn anything particularly helpful from it which you wouldn't glean from @astavely's paper (the second link above).

The gist of my paper was that we used a "design" subset of the target programming language (an IBM internal systems programming language at approximately the same level as C with inline assembly capabilities - see PL/S if you're interested) with proof rules for each construct in the subset. Specifications could be written (in the Z specification language) and then refined to the design subset with each level being captured using literate programming so a document could be organised to be more readable.

In practice, very few specifications were written (although the use of literate programming turned out to be quite popular).

I think cleanroom software engineering was somewhat more successful, although please note that formal proofs were not usually attempted AFAIK.

The take-away for magma is simply to consider basing it on a subset of an existing language as a way of jump-starting the project.

[blainehansen]

Thank you so much for your feedback! You're absolutely right the scope of the project might be too ambitious, and this kind of wisdom is exactly what I'm looking for in sharing this design more broadly. When I get a chance I'll read these papers and think about what you've said.

[dumblob]

@glyn just FYI there is at least one fully dependently typed language which transpiles to a well-established language (JavaScript). It's Kind and I really like how they approach the problems dependent typing brings (though it still requires manual proofs from time to time). Might be worth taking a look at.

[blainehansen]

@glyn I've been chewing on this, and I think you're absolutely right that it would be very difficult to write every layer from whole cloth. The scope of the project is the biggest risk, mitigating it in any way that remains consistent with the goal is crucial.

I think I'm circling around using a subset of LLVM itself as the first bootstrapping language, to piggyback on all the assembler backends and optimization work available in the project. Then to stay sane and avoid having to write the whole thing in LLVM, I'd write "rough and ready" higher level constructs intended to be unfolded and rendered at the Coq level:
https://github.com/blainehansen/magma/blob/main/posts/design-of-magma.md

Or perhaps I could tie the LLVM subset together with something like lambda rust, which already uses Iris, and was created by the Iris main author?
https://www.ralfj.de/research/thesis.html

That certainly seems like it could work, I don't know why I'm hesitant about it.... perhaps just because my hope for the project was to verify the "foundational" layers of the stack? Perhaps because lambda rust wasn't really intended for ergonomic use but for academic work? I've been drafting some questions about this project to send to the Iris main author, I think I'll also ask him what he would think about that approach.

Anyway I'm thinking aloud! Again thank you for your thoughts, I'm sure this design will undergo a huge number of changes as I push through it ha.

[blainehansen]

Yeah @glyn for now I'm going to make Magmide output runnable LLVM, and slowly add concepts and formalization. Lambda-Rust may come in to the mix at some point, but it seems more aligned with the project goals to start at the LLVM layer.

Thank you for pushing me to be pragmatic!