So, that makes me notice I didn't clearly explain, that my idea here would be for some kind of guard blocks that
enforce static typing (etc.) in some areas of code. Kinda similar to "unsafe" in Rust: ideally, you could start with e.g. fully dynamically typed code, then mark some parts of it with "I want this area typechecked", finally requiring all of it to be. Now that I think of it, seeing that in statically typed languages you can kinda already do this (with "Any" type, or "void*", or "interface{}", or whatsit), you could e.g. imagine marking some code blocks with a pragma "any=default" or "any=allowed" or "any=forbidden". So:
- "any=default" - marking the block as dynamically typed and not needing type annotations everywhere (but maybe allowing them if I want, and typechecking then if possible?) - modulo any inference;
- "any=allowed" - marking a block as "statically typed" with type annotations required, and "Any" allowed ("classical static typing");
- "any=forbidden" - would mark the block as statically typed with "Any" not allowed at all.
I'd then start by coding with whole codebase being "any=default", making it work like in JS/Python/Lua/...; then if happy with the prototype, I'd switch the whole codebase to "any=forbidden" and have the compiler force me to add type annotations. Finally if I know in some areas I really want the "Any", I'd mark some small blocks with "any=allowed", working as kinda "unsafe" marker in Rust. (Obviously, subject to bikeshedding over the specific pragma naming & modes.)
Similarly, I'd like to have another pragma for errors handling strictness (regardless whether actual error handling is done in a Rust-like "Result" way, in Go/Lua-like "soft-Result" way, or in an "exceptions" way), and for proving.
