IEEE 754 Representation

Is it okay to use lower bits for a type tag?

Yes if you don't need the precision... which is probably the case if you're using floating-point anyway.

>>2

You can typecheck a program with just pencil and paper, without ever running it.

You can also "run" the program with pencil and paper. (What do you mean you need a computer...? What the fuck are they teaching kids these days...!?)

2. Stop dividing computation into compile-time and run-time. It is a false dichotomy.

For me, anything that needs input is run-time, and anything else is compile-time. (You academic intellectual masturbators are probably going to disagree but that's how it works in practice.)