[skulk]

> What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code

This doesn't even exist in TypeScript. If I change

    function foo(a: any) { return baz(a); }

to

    function foo(a: number) { return baz(a); }

whoever calls foo has to still prove (or assert) that the argument is a number.

Is that what you're after, asserting a dependent type? For example being able to change:

    function divByTwo(a: number): number { return a/2; }

to

    function divByTwo(a: even_number): number { return a/2; }

You want every place divByTwo is called to also automatically supply a proof that the argument is even?

[valyagolev]

i don't even need it to go beyond the insides of a function. something like a proof of an invariant that's only relevant inside the function's body would be fine. e.g. in Rust, almost every place where you see something like ".unwrap()" with "// unwrap safety:" comment, this comment could be an assertion easily proven from the few lines above