[Haskell-cafe] Well typed OS
jo at durchholz.org
Sun Oct 7 11:10:17 UTC 2018
Am 07.10.2018 um 12:41 schrieb Ionuț G. Stan:
> The JVM is also doing something similar. There's a step in the process
> of loading the .class files called "bytecode verification". Ιt's
> basically a type checker for the stack language used in the bytecode.
It's checking more than just types:
* Branch target and exception handler address validity.
* Stack offset validity.
* Each code branch ends with a return instruction.
* Local variables initialized before use in each branch of code.
* No stack overflow or underflow along each code path.
* Validation of private and protected access.
I suspect that all of this can be expressed as a type check, but some of
them require that a type be generated for each natural number that's in
the class file, and I have yet to see an approach that gives each of
these types a printable, humanly understandable representation.
More information about the Haskell-Cafe