4 ms·
So, IANAPLT, and I think that must be definitely clear now if it wasn't enough so before... but then, who says I can't dream! :D and in this dream of mine, thos
by akavel 5y ago
So, IANAPLT, and I think that must be definitely clear now if it wasn't enough so before... but then, who says I can't dream! :D and in this dream of mine, those things seem to indeed be lexically scoped, apparently... :) As to the next thing, I feel I don't understand completely the details of what you wrote in the ETA section, but wouldn't it be similar like with unsafe in Rust? AFAIU, it's on the writer of the code in the unsafe block to ensure that whatever leaves the unsafe zone, it has its invariants all buttoned up and behaves properly back in the civilised world.
As for not being trivial, I kind of maybe have to understand (I found esp. Hishamhm's presentations about the design and evolution of the Teal language, née TL a.k.a. Typed Lua, enlightening yet approachable in this regard); yet, again, IANAPLT and I can dream :) and who knows, maybe some actual PLT will look at it and say, whaa, hmmm; but is it really for sure impossible? I. AM. CURIOUS..... <cue ominous thunder>
- wk_end 5y agoWell, all I mean in the "ETA" is that if you want very robust guarantees about type safety - more robust than Rust's notion of safety - then you're going to be very, very restricted in what you can do. OTOH, if you're fine with looser guarantees about correctness, I'm not sure if marking blocks as safe/unsafe really gets you much more than Typescript, which does (with strictness turned on) force you to be explicit whenever you're using anys. And it's unclear how you can "button up" dynamic data and pass it back to the civilized world.
- 2143 5y agoWhat's IANAPLT? I googled and got nothing.
- akavel 5y agoI Am Not A Programming Language Theorist (Theoretician?...)