Hacker News Reader

Comment by kentonv | Hacker News Reader

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

View on HN

I dunno. Have you used Elm? I hadn’t until recently, but after getting past the learning curve, I honestly can’t recommend any more safe/painless framework for a web FE. It hasn’t been updated in a while, but to me this is a feature, again: its surface area is thin enough that there haven’t been any security issues in the same code for half a decade, and code from that long ago still works today.

I maintain a React app on the side, and a few other projects, and would still recommend it just due to developer availability, but there’s a saying among some of the Elm folks I know: “Good React code in 2025 looks like good Elm code from 2015.”

(To be fair: teams, and devs new to FP [myself included] will create complexity monstrosities in any paradigm, but Elm’s strong FP setup means huge subsets of those monstrosities won’t ever compile, and usually offer a clearer path for later cleanup.)

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

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.

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

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?

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

Reply on news.ycombinator.com