abathologist

I think it was indeed use of GPS that first made me aware of how much the systems we are building are trying to automate me. From the socials to Jira to slack GitHub to crypto to GenAI... it is now painfully obvious that all these systems are pressing upon us to react to stimulus in predictable ways to execute a part of some larger movement which -- probably -- no one has actually designed or considered the purpose of.

I think we are in the third act of a very long play:

> If mechanical thinking and ingenious experiment produced the machine, regimentation gave it a soil to grow in: the social process worked hand in hand with the new ideology and the new technics. Long before the peoples of the Westenr nworld turned to the machine, mechanism as an element in social life had come into existence. Before inventors created engines to take the place of men, the leaders of men had drilled and regimented multitudes of human beings: they had discovered how to reduce men to machines. (https://en.wikipedia.org/wiki/Technics_and_Civilization)

> Personal transformation is as significant, if not more

I would include personal transformation. I think it should be clear that my point is not against "production-oriented pastimes" in any way.

> It's about doing for the sake of being.

Yea, this is totally aligned with my view too. I'd just note that being is not separable from becoming and changing.

I'm afraid you either didn't read me well, or I didn't write my intended sense well, or both. But I think we are pretty much in agreement in any case, assuming I understand what you've written here :D

The surrender is largely voluntary, and is especially enabled by those who think "the systems" somehow know the "best outcomes".

I think we are going to be seeing a vast partitioning in society in the next months and years.

The process of forming expressions just is the process of conceptual and rational articulation (as per Brandom). Those who misunderstand this -- believing that concepts are ready made, then encoded and decoded from permutations of tokens, or, worse, who have no room to think of reasoning or conceptualization at all -- they will be automated away.

I don't mean that their jobs will be automated: I mean that they will cede sapience and resign to becoming robotic. A robot is just a "person whose work or activities are entirely mechanical" (https://www.etymonline.com/search?q=robot).

I'm afraid far too many are captive to the ideology of productionism (which is just a corollary of consumerism). Creative activity is not about content production. The aim of our creation is communication and mutual-transformation. Generation of digital artifacts may be useful for these purposes, but most uses seem to assume content production is the point, and that is a dark, sad, dead end.

What kind of problems are you solving day-to-day where the LLMs are doing heavy lifting?

OCaml has had great concurrency support for years and years. Multicore is only a question of shared memory parallelism.

OCaml has utop, down, and the unadorned ocaml top-level.

Any one know how Curry (which has a Haskell-like syntax extended to support prologish features) compares with Mercury (which has a Prolog-like syntax extended to support Haskellish features)?

There are important exceptions, such as C.S. Peirce, Whitehead, and currently Robert Brandom.

William Lawvere is also a post-hegelian.

Perhaps I misunderstand, but your criticism seems to me rather to agree with Penrose's argument. Points (1) and (2) argue that human reasoning is not computational, in the sense relevant for Gödel's theorems. That is exactly Penrose's point (and was Gödel's point too). He's arguing that we are not going to get a fundamentally super-computational system thru a stack of computations, no matter how big your stack gets. You seem to be confirming this.

I don't understand how you mean (3) to apply as a criticism at all. He is not making a claim about truth at some level, he's just reminding us what computation is and what its limits are.

afaiu, there are two ways to counter Penrose's claim:

a. Prove that consciousness is actually just computational.

b. Prove that merely stacking computations can somehow produce a super-computational system.

You can do [model based testing](https://en.wikipedia.org/wiki/Model-based_testing) (e.g., https://mbt.informal.systems/)

But this exact problem is why I am more interested in approaches that integrate specification and implementation into a single (dialectical) process (e.g., via type-theoretic methods).

The hubub around the Gettier paper is surely among philosophy's most shameful moments.

> This repository is a package repository for the opam package manager. It contains OCaml with Jane Street language extensions, including all Jane Street packages and necessary patches to external packages for building our libraries.

Key features of note include

- Locality via modal types - Layout polymorphism for polymorphic unboxed types

See https://blog.janestreet.com/author/mslater/ for more.

> Why is this taken as a given to be a good thing?

Aspiring to rigorous reason and maximum reasonability is necessary for virtue. Maths is the way we reason rigorously about space and time.

Yeah, I thought the same!

I am not much concerned with hyper optimizations, but I was curious how OCaml would fair with the initial, simple steps, before things get crazy. But I opted for a more complex program:

    (\* t.ml \*)
    let () = print_endline "Hello, World!"

Then just doing a standard compilation and a strip:

    $ ocamlopt -o t t.ml && ls -l -h t | cut -d " " -f5
    1.5M
    $ strip t && ls -l -h t | cut -d " " -f5
    356K
    $ ./t
    Hello, World!

I may be overlooking something, and would be interested to learn what if so, but I was surprised we got a result smaller than the rust binary in the first instance.

> I don’t recall people striking up conversations in grocery lines before smart phones, nor would I have been interested in it.

I do. You may not quite be old enough to have seen/participated in this. Or maybe it wasn't happening where you live for some reason? (E.g., this was probably more common in the urbs than the sub-urbs, due to other alienating forces in the latter).

> people also downplay how much smartphones just replaced rampant TV consumption for people who like to be entertained constantly

It was (mostly) not possible to have a TV with you at all moments, on the bus, in line, in the toilet. This meant lots of times where people were with their thoughts or one another. Also, phones have not replaced TV but overlay it. Many (most) now watch their TV (even if streaming) while also layering distraction from their phone.

> Personally, I handle smartphone usage just fine as do most of the adults around me.

Good for you! I'm curious, what's your average phone usage in hrs/day?

IMO, the degrading effect of smart phones (and the distraction machines of the attention economy more generally) is something that should be discussed and problematized. If some are good at self-moderating, their contributions to the discussion may be especially helpful.

> I reject the idea that all techies need to reject technology and smartphones

Just to clarify, rejecting smart phones as they are currently designed and implemented as bad technology is not the same as rejecting all technology per se.

> projecting their own solution on to everyone else is about as appealing as the person who had a problem with drinking too much trying to insist that nobody else should drink any alcohol at all either

This is an interesting analogy b/c ["No level of alcohol consumption is safe for our health"](https://www.who.int/europe/news/item/04-01-2023-no-level-of-...). I doubt that smart phones are as unequivocally toxic as alcohol, but I do suspect that the current way they are used and developed may be, esp. thanks to gamification, nudge design, and surveillance. Research is coming out on this, but I think there is good reason to not assume it is systemically innocuous as you think it is.

However, b/c living in an inattentive society may actually be worse for everyone, it's possible that a better analogy may be smoking in public or drunk driving: if you smoke in public places or get behind a wheel, everyone is at greater risk.

> I also use my smartphone for important things like maps, taking photos, keeping lists, and even paying for groceries if I forget my wallet.

Imagine a utility that enabled these important functions but did not also constantly disrupt your attention with push notifications, harvest your data, or present the temptation of hours wasted in toxic digital fun-houses! :D It's possible!

This is an interesting reflection, and I'm glad to have read it.

A few things came to mind:

The view of programming as "summarizing what's on StackOverflow" is really alien to me. I suspect this is indicative of a particular approach to programming, and perhaps to working in general, which I don't share. The author's view seems to be that knowledge exists "out there" and the role of the "knowledge worker" is to accumulate, internalize, and reshape it into products derived by summarization. Compare this with another view on "knowledge work" taken from https://en.wikipedia.org/wiki/Knowledge_worker

> Nonaka described knowledge as the fuel for innovation, but was concerned that > many managers failed to understand how knowledge could be leveraged. Companies > are more like living organisms than machines, he argued, and most viewed > knowledge as a static input to the corporate machine. Nonaka advocated a view > of knowledge as renewable and changing, and that knowledge workers were the > agents for that change. Knowledge-creating companies, he believed, should be > focused primarily on the task of innovation.

High value knowledge work involves creating and transforming knowledge, not just compressing or reconfiguring it.

To expand on this in abstract terms: knowledge work is fundamentally cognitive and it gets its higher order purpose and potential from the application of reason; i.e., it is concerned with rational cognition. Rational cognition is mainly about synthesizing new, higher order concepts that direct and evolve given concepts into more general and potent structures. This work involves re-cognition as a necessary component, but if it were only recognitive -- as it would be if were only concerned with recollection and summarization -- it would not have the creative dynamic which it does.

To expand in more specific terms: programming work involves problem solving, but it is not mainly about reassembling existing solutions to solve known problems. The most valuable aspects of this work come from problem discovery, root cause analysis, and solution invention. (Programming work that consists in StackOverflow copy pasta is probably best viewed as the production of tech debt :) This is not to say resources like StackOverflow arent useful, they definitely are!)

I suspect it says more about the author's career aspirations and the reigning interests of the political-economic system that they envision a future where everyone is a manager. First, only if you have "manager brain" can you look at what's happening in tech and see a future where everyone is a manager as a positive development, when compared with a future where everyone is a researcher, artists, arisen, inventor, etc. Second, the managerialization of work is actually describing an idealized view of the present situation, and if it is looming in the future it is only as an intensification of the current dynamics. The rise of [the Professional Managerial Class was heralded in the 70s][1], and most tech workers are in the PMC:

> Who are these Americans working in the upper echelons of the knowledge > economy, exactly? ... the Professional Managerial Class. The PMC, as they are > now often called, came into existence in the late nineteenth and early > twentieth centuries. They were not the old petty bourgeoisie of small-business > proprietors and independent farmers, but a new class whose expertise was > required to make an industrial economy function: engineers, scientists, > teachers, doctors, social workers, functionaries, bureaucrats, and other > professionals and managers who had the know-how to create and control the > levers of the modern capitalist world [0].

The managerialization of everything does seem very likely, because that is basically what our current economic regime has been trying to achieve since the advent of the "digital revolution" (and maybe since Hobbes: a pyramid scheme of nested managers, where every managed worker is actually a manager automating its own autonomous subordinates).

Against the view that computers are a tool for rendering every "maker" into a "manager", I propose meditating on the view propounded by Conal Elliot that computers should be "telescopes for meaning".

[0]: https://pages.cs.wisc.edu/~remzi/Naur.pdf

[1]: https://www.michaeljkramer.net/ideas-of-the-pmc/

$$$$$

> Physical property is a consequence of the laws of physics. If I have a gold coin in my hand, then you don't have that gold coin in your hand.

So do you believe people should only be able to own real estate that they are currently physically occupying? By your reasoning, no one could ever own a piece of land larger than what they were currently standing or lying on. So no one could own land. So abolition of all property rights, essentially.

I'm hella down for this, but then we should also be able to walk into the OpenAI offices and inspect their source code, cause that shit won't fit in any one hand afaik.

This is incredibly naive misunderstanding of how property rights work: they are 100% a social and conceptual construct. IANAL, but I believe you are confusing property with possession.

But, yeah. I'm down: no one can own anything that isn't currently in their hand. Let's go liberate a lot of fake property that is "owned" in violation of the laws of physics!

CORRECTION:

> find and diagnose typing errors prior to running any type checker

Should read

> find and diagnose typing errors prior to running any model checker

That's what I meant! Thanks for the correction :)

I think you and Ron are confusing the relevant phase distinction the rest of us have in mind when we talk about type checking in this context.

What we mean is that quint, the language, is expressed on top of a many-sorted logic which allows our tooling to find and diagnose typing errors prior to *running* any type checker. The TLA Toolbox doesn't support this, and TLA+, like TLA itself, is untyped. TLC can (and will) raise errors while in the process of checking your model due to the kinds of problems we usually call "typing errors". Quint and apalache shouldn't do this.

I hope this helps clarify a bit.

We understand that, viewed purely theoretically, TLA+ has no dynamic aspect at all, etc. However, our team is very focused on the fusion of theory and practice, and we think it's important to ground our understanding and our discourse in the way the specification languages are actually used by real people given the existing tools. While it may be true in theory that

> What TLA+ is missing is any notion of executing code.

The file `TLC.tla` in the `StandardModules` includes these lines:

  ```
  Print(out, val) == val
  PrintT(out) == TRUE 

   (* This expression equals TRUE, but evaluating it causes TLC to print   *)
   (* the value of out.                                                    *)   
  ```

https://github.com/tlaplus/tlaplus/blob/master/tlatools/org....

In any case, our whole team thinks TLA is great, and we're happy people like you and Ron find it so useful and insightful. We also think it is a very insightful tool for guiding understanding :)

This is great feedback, thanks! Probably the first step tutorial should just be on something very straightforward, like an hour clock or a counter. I'll file an issue to introduce something more focused.

Thanks again :)

edit: https://github.com/informalsystems/quint/issues/1319

Those are great questions! Let me add a one addendum to bugarela's excellent explanation, to help disambiguate these three formalism:

1. TLA[0] is a logical calculus invented by Leslie Lamport.

2. TLA+[1] is a formal specification language, also invented by Leslie Lamport, with semantics based on and reducible to TLA.

3. quint is also a formal specification language with semantics based on and reducible to TLA.

TLA+ can be understood as TLA extended with syntax sugar to help describe systems. On top of the logical calculus it adds niceties like `LET` bindings, syntax to represent common data structures, `CASE` expressions, a module system, etc. But TLA+ also exposes the underlying logic directly, making the language extremely expressive. The flip side is that nonsensical formulas which may not be checkable are pretty easy to write.

quint is a (programmer friendly) syntax that, while also desugaring to TLA, gives up expressivity to add the guardrails that we've found most helpful when specifying the systems we work on.

Please let us know if you have any followup questions :)

---

[0]: https://en.wikipedia.org/wiki/Temporal_logic_of_actions [1]: https://en.wikipedia.org/wiki/TLA%2B

I can sympathize! We are aiming to maintain most of the expressive power of TLA+ -- ideally everything you need for a concise, high-high level specification, that can be simulated and/or verified -- but with surface syntax that is more approachable coming from a programming background. If you're interested in seeing how it maps to TLA+, you can find much of that in this document: https://github.com/informalsystems/quint/blob/main/doc/lang....

We still have lots of ways to improve, and -- we think -- lots of opportunities to improve our interop and complementary qualities in relation to TLA+ and TLC. But we have found the tools in their current state useful enough to be worth sharing :)

That is our aim! If you give it a shot and find things that aren't so approachable, we'd live to hear how we can improve.

That page seems totally reasonable and admirable to me. It’s literally just advocating for including the wide and varied history of algorithm development, in order to encourage readers from many different backgrounds to find ways to connect with the important topic.

It's still in pretty early development, but you may be interested in https://github.com/informalsystems/quint

> It combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.

And it is typed ;)