search

andrew-johnson-4 / lambda-mountain

Tiny Functional Language Compiling to Assembly (7000 Lines of Code)
https://andrew-johnson-4.github.io/lambda-mountain/
MIT License
17 stars 0 forks source link

Preconditions / Postconditions #378

Open andrew-johnson-4 opened 4 months ago

andrew-johnson-4 commented 4 months ago

Types may imply preconditions or postconditions that perform limited computation.

andrew-johnson-4 commented 4 months ago

This can be used to validate register allocation and memory model etc. Nominal trust is not the end of verification.