search

andrew-johnson-4 / lambda-mountain

Compiler Backend for LSTS (Typed Macro Assembler)
https://andrew-johnson-4.github.io/lambda-mountain/
MIT License
20 stars 1 forks source link

Formal assertions on fragment shape #773

Open andrew-johnson-4 opened 1 month ago

andrew-johnson-4 commented 1 month ago

What does a U64+LocalVariable fragment look like? What is expected of it?

There can be rules for fragment shape by type which would serve to sanity-check fragment functions and also can help to generate Coq proofs.

andrew-johnson-4 commented 1 month ago

https://andrewjohnson4.substack.com/p/a-new-programming-idiom-emerges