search

andrew-johnson-4 / lambda-mountain

Terse Typed Macro Assembler (4000 Lines of Code) DRY your code in any language
https://andrew-johnson-4.github.io/lambda-mountain/
MIT License
17 stars 0 forks source link

Certify memory model with Coq #633

Open andrew-johnson-4 opened 2 months ago

andrew-johnson-4 commented 2 months ago

From start to finish for every single code block.

andrew-johnson-4 commented 2 months ago
  1. Compiler generates human readable gnu assembly with type annotations
  2. Associated tool extracts annotations into a Coq verifier
  3. Coq verifies proof

The Intermediate assembly doesn't depend on LM frontend this way

andrew-johnson-4 commented 2 months ago

The lmv tool should be a thin client only to parse assembly and generate coq terms. Things like assertion interpretation should be modelled entirely in coq.

andrew-johnson-4 commented 2 months ago

Assertions should be given blame information in case they fail.