cakeml
cakeml copied to clipboard
Add some basic static checks to the Pancake compiler
It would be nice if the bootstrapped compiler would reject Pancake programs:
- where out-of-scope variables are mentioned, and
- with missing return statements.
I don't think there's any particular benefit to proving any theorems about these passes, since they do not suffice to imply the absence of runtime failures. But it would remove some pointless foot guns for people who use the bootstrapped compiler.
The first of these has been addressed by #986