Throwing a theorem-prover at the problem, unaided by developer hints, is not realistic in a large codebase. You need annotations that let you say "this array's size is is the same as that array" or "this integer is within the bounds of that array" -- that's dependent types.

▲

instig007 4 days ago | parent [-]

> Throwing a theorem-prover at the problem, unaided by developer hints, is not realistic in a large codebase.

Please, Kenton, don't move your goalpost. Who said about "unaided"? Annotations, whether they come directly from a developer, or from IR meta, don't make a provided SAT-constraint suddenly a "dependent type" component of your type system, it needs a bit more than that. Let's not miss the "types" in "dependent types". You don't modify type systems of your languages to run SAT solvers in large codebases.

Truly, if you believe that annotations for the purpose of static bounds checking "is not realistic in a large codebase" (or is it because you assume it's unaided?), I've got "google/pytype" and the entire Python community to justify before you.

▲

kentonv 4 days ago | parent [-]

Ah you are just trying to gaslight me. pytype doesn't do static bounds checking.

What compels you to do this? Posting just to make people angry? Do you not have anything better to do with all that PL theory expertise?

	▲	instig007 4 days ago \| parent [-]
		> Ah you are just trying to gaslight me. pytype doesn't do static bounds checking. It does static type checking from _annotations_ that live _outside_ the type system of the language. Have you forgotten that you began to argue that SMT solvers need constraint annotations to be realistic for static bounds checking in large codebases, and that the constraint annotations somehow become dependent types from that fact alone? > What compels you to do this? Posting just to make people angry? Do you not have anything better to do with all that PL theory expertise? You're all over the place, it's frustrating that instead of fairly addressing the points about inferior aspects of the protobuf protocol design that are unnecessary for the purpose of backward-compatible distributed systems, you keep saying (or at least assuming) that it's the only realistic solution, because "I worked at google" and "reports at google prove me right".