[valyagolev]

I totally share your excitement about dependent types, but it seems that, unlike the type systems we're used to, theorems about the dependent types are much harder to prove, which makes them not very comfortable to use for the whole program.

If only there was some kind of a gradual, perhaps typescript-like approach to adding arbitrary type-level value-limiting information in random places without having to have everything proven everywhere...

[skulk]

Every non-dependent typing relation is also a dependently typed relation so I think things are already the way you want, unless you have a certain example in mind.

[valyagolev]

Sure, in the same sense that every "untyped" program is already typed with some kind of a universal type, but what's the point?

What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code without necessarily making sure that every possible presupposition is proven from the ground up. Just like in Typescript, I can add a type at any point where there was only "any", and have a small portion of the program typed without typing the whole thing

[dunham]

Not sure if it's what you're asking for, but in lean, you can put `sorry` to skip a proof. It's `believe_me` in Idris2, and I think the Agda version is `trustMe`.

You can also use stuff like ! when you don't want to prove your array indices (it might crash or substitute a dummy value if you're wrong).

[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