[Haskell-cafe] Well typed OS

[Ionuț G. Stan]

On 07/10/2018 14:10, Joachim Durchholz wrote:
> 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:

Sure. I used an informal, hand-wavy sense for "type checker".

> * 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.

Can you give a bit more detail here? Or a pointer to someone who 
elaborated on this? I got a bit lost on the natural number step, which 
seems to be some sort of theoretical way to represent those types. On 
the other hand you say they're in the class file.

BTW, I'm quite familiar with the class file format and have even started 
writing a bytecode verifier for my own compiler pet project. So, be as 
specific as you can.

> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
> 

-- 
Ionuț G. Stan  |  http://igstan.ro  |  http://bucharestfp.ro