Eggplant.place

Regarding the LB, https://fedi.kbg.sh/users/kevin/statuses/117085582358711627

There's an interesting thing about strongly typed programming languages, especially dependently typed ones (1), wherein if you know the type signature of a function there is sometimes only one implementation of it, and that implementation will have lots of nice properties (e.g. Philip Wadler's Theorems for free! paper, also Jose Oliveira's work, and the followups to these). It's a fascinating set of results that holds out the possibility of at least some amount of automatic programming that has desirable, provable properties concerning correctness, resource use, security, and so on.

However, that "some amount" is very important to remember. I'd argue that no matter how far such work is pushed, there will always be an infinite space of things one might wish to express in software that cannot be automatically programmed in that way. That's the Therac-25 space the LB evokes. We all know this intuitively, I think, yet in the various mystifications thrown up about computers and software and now LLMs it can be hard to remember.

For example, I'd say so-called "side effects" or just "effects" are still a large blind spot of these methods. Without effects functional programming does little more than heat up a CPU (but the heat is an effect oops), so if we're being snarky we might say functional programming without effects isn't programming at all. But in spite of the gazillion attempts to do so, you really cannot faithfully capture all side effects of interest in a type system, for the simple reason that the real world is open-ended.(2) There's a funny contradiction that functional programming languages could not exist were it not for irreducibly effectful computational architectures to exist on. Asking the CPU to execute an instruction, and all the statefulness this necessarily involves, is a "side effect" in this view of computation, which is absurd.

For these reasons I've found it fruitful to conceive of functional programming as an intricate bureaucracy sitting between the programmer and the real world.(3) Set up enough bureaucracy and you can comfortably pretend most of the real world isn't there most of the time. Some people do this for so long that they begin to think the bureaucracy is the real world (4); or they try to warp the real world till it becomes more and more like the bureaucracy.(5) But the real world is oozy and eventually squishes around all attempts to constrain it in this way. Neglecting this is how people end up being harmed by digital technology.

#AI #GenAI #GenerativeAI #LLMs #Lean #math #ComputerScience #theory #FunctionalProgramming #philosophy

(1) "leanslop" in the linked post refers to Lean, a dependently typed functional programming language that's being used to formalize mathematical ideas. We should always remember that Lean originated from Microsoft Research
(2) There's a long history of philosophical arguments hiding behind that assertion but there's no space to get into that here. A less contentious way to put it would be that the claim that all side effects worth caring about can be captured in a type system is a philosophical commitment, not a fact about the world, and therefore it's possible it cannot be done
(3) We use terms like runtimes, preludes, standard libraries, or APIs/ABIs (among others) for this bureaucracy
(4) "Touch grass"
(5) Financialization and neoliberalism, e.g.

Edited 89d ago