I've actually been building a teaching VM with these properties. You can't take the address of arbitrary values (so there's no distinction between lvalues and r

I've actually been building a teaching VM with these properties. You can't take the address of arbitrary values (so there's no distinction between lvalues and rvalues), there's no pointer arithmetic (instead you have type-safe primitives for record access and array indexing), all arrays (including strings) know their length and bounds-check accesses, and unions behave more like sum types, always knowing precisely what type they have stored. All these constraints ensure you can never convert a number to an address, or generate an address to an illegal value. More info about the goal and rationale: http://akkartik.name/post/mu; http://akkartik.name/post/mu; http://github.com/akkartik/mu http://github.com/akkartik/mu. I also recently found out about http://eigenstate.org/myrddin http://eigenstate.org/myrddin which seems more mature with very similar goals/aesthetics. I've been digging into it a fair bit. Finally, on the extreme other end of the spectrum, there's Rust.