[Haskell-cafe] Well typed OS

[Joachim Durchholz]

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.