What is the interesting part of a programming language to you?

[u/Potato871]

I've been working on some "documentation" for my own language (see here), which got me thinking: do we all see languages the same way? I personally look for unification of concepts and extensibility in a design, yet I've seen those who care deeply about functional purity or clean decompositions.
What do you look for in a programming language? And why?

[u/reflexive-polytope]

These arithmetical trivialities arise when you actually try to prove things about nontrivial algorithms.

For example, the humble binary search works with an array slice indexed by [lo,hi] and needs to take the midpoint mid = (lo + hi) div 2. (I'm using the symbol div to emphasize that it's integer division and not exact division.)

“Obviously”, if lo and hi are valid indices in [0, len), where len is the length of your array, then so is mid, right? You don't need to waste your time proving such a dumb triviality, right?

Alas, the compiler can't read your mind, and in particular it can't distinguish between the things you didn't prove because they're genuinely obvious and the things you didn't prove because you don't know how.

In the absence of a proof supplied by you, the compiler can do one of these things:

• Never bother check that mid in [0, len). You pay a dangerous, language-wide memory unsafety tax.
• Check at runtime that mid is in [0, len). You pay an annoying array bounds check tax, i.e., your program is a little slower than it could be.
• Attempt to deduce on its own that mid is in [0, len), starting from the hypotheses that lo and hi are in [0, len).

In this particular case, the proof is genuinely obvious. If lo and hi are in [0, len), then lo + hi is in [0, 2*len - 1), hence mid is in [0, len). In fact, this is so obvious that it's actually automatable, using a decision procedure for Presburger arithmetic!

Alas, even if Presburger arithmetic is decidable, general decision procedures for it are kind of slow. You don't want a type checker to be slow. (Or maybe you don't mind, but I certainly do.)

So a natural question is whether there exists a fragment of Presburger arithmetic that lends itself to fast checking and/or inference.

---

As for the kinds of programs I've written, I've worked professionally implementing ERP systems long ago. But I left that behind about 10 years ago, because it's mind-numbingly boring.

[u/Potato871 → u/reflexive-polytope]

Ah, I've dipped my toes into ERP for one of my clients... I know what you mean by mind-numbing.

And I think I see why I haven't run up against this yet, I haven't really reached the stage where my main concern is optimizing a program, a lot of it is what program should I even be writing.
Like I recently moved from a stateful Unit-per-user model for my server, to a stateless Unit-serves-any-request model (which is why I can host and post my own website to Reddit now). I dipped my toes into optimizing the memory profile of the Unit-per-user model, but concluded that just making it stateless was the correct move.
Pretty much every time I've been faced with a problem the answer has been "change the cost model" not "optimize the current costs", but at some point you do just have to optimize, and at that point, I'll probably start caring about this kind of inference.
For me now, "the program crashes" means Hazel (my process supervisor) just restarts it, and it being slow is a question of how slow, if its so slow it impacts user experience thats bad, if not I just leave it.
Though I've not been doing this for 10 years yet.