> type algebra either doesn't exist or impractical because only PL theorists know about it, not Kenton.

Hi I'm Kenton. I, too, was enamored with advanced PL theory in college. Designed and implemented my own purely-functional programming language. Still wish someone would figure out a working version of dependent types for real-world use, mainly so we could prove array bounds-safety without runtime checks.

In two decades building real-world complex systems, though, I've found that getting PL theory right is rarely the highest-leverage way to address the real problems of software engineering.

▲

instig007 4 days ago | parent [-]

> Still wish someone would figure out a working version of dependent types for real-world use, mainly so we could prove array bounds-safety without runtime checks.

Hi Kenton, I'm not sure what kind of PL theory you studied in college, but "array bounds-safety without runtime checks" don't require dependent types. They are being proven with several available SMT solvers as of right now, just ask LLVM folks with their "LLVM_ENABLE_Z3_SOLVER" compiler flag, the one that people build their real-world solutions on.

By the way, you don't have to say "real-world" in every comment to appeal to your google years as a token of "real-world vs the rest of you". "But my team at google wouldn't use it", or something along that line, right?

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML...

▲

kentonv 4 days ago | parent [-]

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".