In Context
12 points by veqq
12 points by veqq
Summary in progress
First, our prophet says the majority of programmers work on "information programs" where one e.g.:
Information programs have many concerns, mostly around keeping formats, correct procedures and channels, besides returning the right answer. He doesn't think static types are a good fit for these, but excel at inherently internal "mechanisms". Although this lends confidence when plugging in two things with the same connector, it doesn't work with information; if you had to change all your programs when you add a new column to the database... He notes that many things with different protocols work over eg. usb-c today; flexible systems expect us to get our data format wrong, but allow us to redo and overcome it. Successful, big systems are always dynamic (nature, internet).
How many languages do you use normally? Why use a language for this which just gives you mechanisms but not the basic ones you need every day like hashtables? You'll constantly be dealing with impedance mismatches, pipe together different formats. Clojure is good here (but some counterpoints.)
Then he returns to points from past talks.
Context is etymologically "weave together", i.e. the same as complex.
Checking keys in destructuring (via the :keys! "directive") helps with documentation (by requiring them) and helps you specify what you expect. "Breakage is bad." There's a fair bit of explanation about the new system with some new terminology like "binding list" directives.
More interestingly, he mentions that people expect schema things like spec to say something's wrong if you don't have so and so, but he rejects this brittle approach. Instead, he suggests this system says "you have to give me what I need". I think this is basically just saying that a hashmap or table with many keys/columns can change a lot, but programs work fine with it because they just look those up. He uses a selection within comments:
(let [{name ... }]
;; bindings
;; name, city, nickname
;; selection
;; :first-name, :address, :nickname, :id, :address -> :city, :zip
The -> means that inside :address he wants to see :city and :zip, the other fields should be in the root.
I agree with this idea, hence my obsession with tables via array languages. But if he's talking about "selection", why doesn't he make a select function? Rich seems so close. @internet_janitor implemented it well in Decker/Lil makes the case well in various places.
the majority of programs are "information programs"
As I understand the video, he is asserting that the majority of Clojure programmers are writing these kinds of programmes (without making any assertions as to the size of the population who write other types of codes.)
supports decision making
As I have presented it (usu. in the context of Python,) the kinds of programmes he is referring to are what I would have labeled as “political” in that they are about encoding some kind of “policy.” (Unfortunately, labelling these as “political programmes” is almost definitely a dead-end: no one will ever understand this terminology as intended; the more common use of that adjective is simply too prevalent.)
The general argument is as follows: many programmes seek to model details of the human world which are formulated and modified in ways which are resistant to typically mathematical reasoning. Whereas what we typically call an “algorithm,” is usually required to be consistent, a “policy” does not need to be consistent. Whereas an “algorithm” is usually constrained in some structural fashion, “policies” are limited only to the whims of the authority setting them. &c.
As a result, it is possible that a type system cannot adequately encode meaningful correctness of a policy (esp. one which has no requirement of internal consistency!) Instead, since the policy is tied to human judgement, we may find that only human verification is sufficient to assert the correctness of an implementation.
Therefore, rather than trying to encode correctness into our type system, it is more beneficial to express the policy in a fashion that is maximally legible to a human auditor, while also maximally preserving flexibility, since the (mathematical) arbitrariness of the policy strongly suggests these may change in unexpected ways at unexpected times and in a fashion that is contrary to the prior design of the system. (Regarding the last point, consider that the aspects of the policy that are of interest to the authority may have no relationship to the way the code is written—therefore, what may be considered a “small but critical” change from the authority's perspective may turn into an enormous change from the perspective of the code!)
As a result, I think it's common to find that this policy code evolves in roughly the direction of a language like Janet or Python (or, I assume, Clojure.)
Here's an small example that I was recently considering: if I want to implement a PAM module, then I will likely want to use a language that can easily interact with C, since modules are shared objects loaded into an application to provide authentication.
I probably don't want to use C itself, since I may be worried that certain correctness that I desire cannot be asserted by the C language and tooling (or, at least, this cannot be accomplished to my satisfaction with a minimal set of tools that I have been using for the last fifteen years…) Therefore, I may desire to use Rust or Zig to write my PAM module, since many important errors will be caught by these tools that will ensure the correctness of my code. Since I know Zig much better than I know Rust, I will use Zig.
However, the actual authentication I may want to implement is likely to have some complexity. If we think about the authentication mechanisms used by smart phones, they're actually moderately sophisticated workflows—fingerprint unless such-and-such condition and then password. If I'm writing my own authentication mechanism, I may discover that I can do something even better—convenience methods that transition into stricter methods under a complex set of conditions, together with duress and rotation and other mitigation mechanisms. I definitely would not want to write this logic in C: it's correctness is likely to derive from the construction of the control flow more so than the correctness that the type system affords me. In fact, even in the case of Zig or Rust, I may struggle to encode anything meaning into the language mechanisms to provide sufficient correctness guarantees (though there are admittedly some things I could do.)
Instead, I may be better finding the maximally legible and maximally superficial way to express the control flow, the workflow. I think a domain-specific language might have been an approach one might have used historically, but the burden of having to design and maintain a domain-specific language is undesirable. (In fact, if we're talking about PAM, we should recognise that the PAM configuration domain-specific language is a somewhat bizarre linearisation of what is otherwise a fairly simple graph—sufficient, required, &c.) So this is a good opportunity for me to use something that is much more flexible, easier to change, and more “legible.” It should be fairly obvious that a language like Python or Janet could be a good choice—Janet is especially quite straightforward to embed—since both can represent the control flow graph in a way that would allow me to visually ascertain correctness (and assert correctness through symbolic manipulation approaches as well as through high-sophistication programmatic/property testing.)
Dynamic languages tend to be pretty good at encoding “policy.”
he is asserting that the majority of Clojure programmers are writing these kinds of programmes (without making any assertions as to the size of the population who write other types of codes.)
Possibly! I changed my phrasing a bit.
Thank you for this framework.
Whereas what we typically call an “algorithm,” is usually required to be consistent
In earlier days, math classes spent much time on easier rules of thumb to greatly speed up calculations to different approximations etc. Sometimes I think modern software cares too much about correctness. Sometimes a few wrong answers are fine, if the overall thing is just more ergonomic; sometimes we can happily make that trade off. The adoption of LLMs seems to show that often people can't even tell the difference.
Unfortunately, I lost buy in very quickly, because his terminology sets up senses of "static" and "type system" that seems totally out of touch with the current reality, as far as I understand it.
Static analysis doesn't mean the system analyzed has to be static which he implies, it covers the properties of a dynamic system that you can analyze by just looking at the system definition. Depending on how expressive the language you use for your definition, you can determine a potentially unlimited set of properties for the defined system over its entire evolution.
The reality is that dependent type systems are just higher order logics with nice computational properties, and then can model and reason about changes over time (temporal logics), about changes in context (context parametric logic), about changes in types over time (type state), about concurrent systems (session types), and distributed systems (choreographic programming).
The clojure features added for data selection and transformation in destructuring seems cool tho!
:all, :select, and :excess as directives seem like philosophically interesting things to drop into core and make convenient. :excess in particular I can imagine is a good building block for ignoring what you don't care about and then merging back in to make sure I don't break downstream code. (Especially with the suggestion at the end that a deep merge is coming to core).
The :missing directive is pretty odd, in that it's hard for me to think of anywhere else in Clojure that the distinction between a missing key and a key that is concretely nil matters much. Feels like I'm going to make a bunch of mistakes on that until I learn not to.