My talk from Strange Loop is out. There will soon be a mini-site with a transcript, references, and a few additional notes and corrections.
Jack Rusher thanks for the talk. More engaging to most. Also I've moved from working on erlang to golang so might be sharing it at the office 🙂
I will be watching this many times more. I think I can probably use it as a shopping list of features to add to my language/editor.
Are they any systems that have done a particularly interesting job of having strong type checking of code that is "Repl'd" into a running system
Great talk. Makes me wish I had gone to Strange Loop now. :simple_smile:
@Peter Saxton Haskell has ghci , but it dumps core surprisingly often (perhaps it isn't correct by construction?). OCaml's utop is better, and the implementors have recently suggested that the current state of the compiler admits further improvements to its interactivity. The team working on Hazel have told me that they'll be exploring live coding in an environment with typed holes in the near future. There are also Lisp dialects — most notably Shen — that support an interesting hybrid way of working; definitely worth checking it out.
As someone who has very much not yet internalized the enlightenment of "debuggability > correct by construction" but wants to, I'd like to make a tangential and simultaneously sadder point.
With modern logging frameworks it's non-trivial to determine if a debug print is working like it should. You don't see a test print, do you have the right logging level, is it logging to the right sink, are the logs from the container making it out of the container, etc., etc. So not only are we still living in the mainframe+teletype era, we're actively moving in the wrong direction. At least when we programmed with teletypes on mainframes we didn't have to worry if a print was getting intercepted before it got on paper.
Kartik Agaram The paper discussed elsewhere (💬 #reading-together@2022-10-08T08:12:59.308Z) provides one response to the question why (and when) "debuggability > correct by construction". Summary: quite often you don't understand your problem space well enough to do "correct by construction". Debugging is not only fixing bugs in the code, but also improving your understanding.
[October 8th, 2022 1:12 AM] chris.shank.23: “Formality Considered Harmful: Experiences, Emerging Themes, and Directions on the Use of Formal Representations in Interactive Systems” by Shipman and Marshall (1999)
> In this paper, we describe how creators of systems that support intellectual work like design, writing, or organizing and interpreting information are particularly at risk of expecting too great a level of formality from their users. To understand the effects of imposing or requiring formality, we draw on our own experiences designing and using such systems. http://www.csdl.tamu.edu/~shipman/formality-paper/harmful.html|http://www.csdl.tamu.edu/~shipman/formality-paper/harmful.html
Jack Rusher interesting mention of propagators here. Are you aware of the "goblins" project of Christine Webber spritely.institute/goblins ?
Seems very intersting to see goblins at the foundation of spritely as a new experiment in the socially networked space
After a frustrating day in the office, mostly struggling to get my debugger to work, I have one possible answer to the question, "why are things not better than in the days of punch cards?"
We don't know how to keep working things working over time, how to keep things from sucking with scale (more users, more use cases). Without that technology -- for the sorts of large applications one typically deals with in commercial settings -- it still seems worth being minimalist with the stack one depends on, that one's application sits on top of.
Like, I'm not sure it's even realistic to expect progress in software tools. Moloch evolves, but in ways that are inscrutable to human values.
(I'll still work on these ideas on the side. But only because I can control application size when I'm working by myself. Moloch ignores me cowering behind my tree stump.)
Trying to reformulate Kartik Agaram's insight in a less depressing way 😉
We have been building more and more complex software over the decades by piling up layer after layer. That makes the lower layers a kind of basic infrastructure that becomes impossible to evolve, because lots of people's uncoordinated decisions depend on it.
Put differently: we still use terminals emulating punched cards for the same reasons that constrain cars to the width of a horse carriage (which is what defined the width of roads).
You can avoid the inertia of the past in a small controlled environment (just you, or a small team). But evolving the mainstream to better infrastructure is a collective action problem - and those are well known to be hard.
Correct, non-trivial constructions come with mastery of the domain — usually after a lot of debugging. Debugging lets you dodge bullets. Correctness is when don't need to. Whether it's even possible to shave off edge cases depends on the substance of the domain.
