[nextaccountic]

but programmers don't write underspecified notational shortcuts, because those are soundly rejected as syntax errors by the compiler or interpreter

this is not about semantics (like dependent types etc) this is just syntax. it works like this in any language. the only way to make syntax accepted by a compiler is to make it unambiguous

... maybe LLMs will change this game and the programming languages of the future will be allowed to be sloppy, just like mathematics

[rq1]

Some compilers can accept “holes” that can be univocally deducted from context for instance.

You can think about it as type inference on steroids.

[nextaccountic]

Yep, but for any notational shortcut the compiler infers a single thing for it. It's still unambiguous as far as computers are concerned (but it may be confusing reading it without context)

[rq1]

It’s not only a notational shortcut as in syntactic sugar though.

It can apply a set of rewrite rules given you were able to construct the right type at some point.

It’s type inference on steroids because you can brute force the solution by applying the rewrite rules and other tactics on propositions until something (propositional equality) is found, or nothing.