official style?

Stream: lean4

[Mac Malone]

I know, Std and Mathlib do not always follow the official style (admittedly, neither does Lake in other cases).

[Mario Carneiro]

well, I would phrase it more as lean core not following the default style :)

[Mario Carneiro]

The most polished documentation we have on style matters comes from mathlib

[Mario Carneiro]

what you are calling "official style" is I think closer to "the house rules of Lean4 repo"

[Mac Malone]

Yeah, no. Lean core is the official style as it is the place where the language is defined.

[Mac Malone]

But, I do agree that we do not necessarily have to adopt its style.

[Mario Carneiro]

For example, lean4 repo doesn't have line limits (or if it does, I haven't found them)

[Mac Malone]

Style, in my view, should be a per-project (or group) thing.

[Mario Carneiro]

std/mathlib style absolutely does

[Mario Carneiro]

sure, it is per project

[Mario Carneiro]

but then you have to clarify when you say "official style"

[Mario Carneiro]

because lean4 repo does not maintain a style guide

[Mac Malone]

I though there was some MD document with some style guidelines, but I cannot seem to find it at the moment.

[Mario Carneiro]

std/mathlib style is to put default files consciously, when we actually intend for import This.Folder to mean something. Mathlib generally avoids it because it is a hazard which causes dependency creep and/or cycles in mathlib, and std uses it to make refactoring possible without breaking imports

[Mario Carneiro]

in neither case are they just stamped out for every directory

[Mario Carneiro]

As another data point, rustc (the compiler) has a very unusual setup for a rust project, and has lots of repo-specific house rules. It is not something you could easily generalize to a normal rust project in the ecosystem. I think this will be a general trend, the compiler is a big project but also an unusual one, not necessarily representative of the average project. Mathlib is also a big project and not representative of small lean projects, but it is very community-focused, and since the style guides invariably come from big projects since that's where the people are, I think it is a reasonably good prototype for a general use style guide.

[Mac Malone]

Which I think is fair. I hold no strong feelings that every directory needs an associated .lean file. I recall that Sebastian did, however, and as one of main designers, I take is word as indicative of official style. I also know that he was big on the no src directory in Lean projects. I stance I personally disagree with (but I have none-the-less adopted).

[Mac Malone]

Mario Carneiro said:

Mathlib is also a big project and not representative of small lean projects, but it is very community-focused, and since the style guides invariably come from big projects since that's where the people are, I think it is a reasonably good prototype for a general use style guide.

Personally, I just do not think mathlib is a good source for general style as it is attuned to the style of professional mathematicians, which is a very beast from that of the style of a general purpose language. Such differences in audiences among different codebases are one of the reason why I think strictly enforced style guides beyond a project or group scope are generally a bad idea. However, I do think code written by languages designers is good for gauging an initial style which subsequent style guides can either embrace or explicitly part ways with.

[Mario Carneiro]

I understand that this is a concern, but clearly the solution then would be to help evolve the style guide in a more domain-agnostic way. Do you actually have any particular style things that you want to point to as mathematician-like?

[Mario Carneiro]

Personally I can't see anything in the mathlib style guide that has clear mathematician bias

[Mario Carneiro]

Here are some stylistic aspects of mathlib, not explicitly in the style guide, which I would call mathematician-biased:

• lots of use of variable
• use of the root namespace
• lots of use of notation
  • especially unicode notation

Is there anything else that comes to mind? These can just be omitted from a general style guide, and none of them really have to do with code formatting, e.g. 2 space indent, 4 space declaration body hanging indent, etc.

[Mario Carneiro]

However, I do think code written by languages designers is good for gauging an initial style which subsequent style guides can either embrace or explicitly part ways with.

We did. The mathlib4 style looks significantly different from mathlib3, because we started with lean4 repo style and adapted it for a general audience. The naming convention is a very obvious example of this: we were mostly fine with the lean 3 naming convention already (partly because mathematician bias is to not care about theorem names), but lean 4 had a new naming convention and we adapted it into a full specification and rolled it out over a million lines of code at great expense.

[Mac Malone]

@Mario Carneiro I just realized I do not know where official mathlib 4 style guide is located. I have visited links to it before, but do not know how to get to it just from the project github itself.

[Mario Carneiro]

Some information is on the porting wiki, e.g. https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention

[Mac Malone]

Mario Carneiro said:

We did. The mathlib4 style looks significantly different from mathlib3, because we started with lean4 repo style and adapted it for a general audience.

Which is great! I was not asserting mathlib did not take that approach, but simply that I think that approach is a good approach.

[Mario Carneiro]

I don't think the rules around indentation are written down, but they are codified in tools like mathport

[Mario Carneiro]

We'll be building the lean 4 version of the website soon, and I expect the style guide to live there eventually

[Mac Malone]

Well, in that case, mathlib style's is about as official as the core's style as core's code style is mostly encoded in the pretty printer. :rofl:

[Mario Carneiro]

there is https://leanprover-community.github.io/contribute/style.html but it is for lean 3

[Mario Carneiro]

mathport uses the pretty printer

[Mario Carneiro]

and no it isn't, core code differs from the pretty printer

[Mac Malone]

As I understand it, the pretty printer is a best approximation of core style that can be done with existing tooling.

[Mario Carneiro]

okay, but mathlib is a more canonical example of "core style" than core is then

[Mario Carneiro]

in particular, when there is a style discussion that results in a change to the pretty printer, core code is usually not updated

[Mac Malone]

(hence the Reformat test)

[Mario Carneiro]

that's testing a very old version of Init.Core

[Mario Carneiro]

it's not even demonstrating that the code reformats to itself, only that it reformats to something in particular

[Mac Malone]

From Gabriel edits/discussions on the pretty printer and that file, that is mostly due to certain limitations in the pretty printer.

[Mario Carneiro]

okay, but it's not justifying the claim that lean4 core passes its own formatter

[Mac Malone]

True, I agree that it does not.

[Mac Malone]

Because the formatter is sub-optimal style.

[Mario Carneiro]

and also lean4 doesn't care about keeping the code format up to date

[Mac Malone]

It is simply the best machine approximation currently available.

[Mario Carneiro]

style change PRs are not welcome, AFAIK

[Mario Carneiro]

mathlib4 is lean4 with a more modern version of the lean4 style

[Mac Malone]

Correct, as Leo more-or-less determines Lean 4 core style and, in fact, has some disagreements with Sebastian on it (e.g. Leo wants parentheses in if (<- x)/match (<- y) and Sebastian is not fond of them), which is why it is not always consistent.

[Mario Carneiro]

right, that's a house style

[Mac Malone]

And my assertion was that all styles are / should be house styles.

[Mario Carneiro]

not everyone can be bothered to write their own style guide

[Mario Carneiro]

plus there is value in having code look similar across projects, so you don't want too much divergence from a common style

[Mac Malone]

True, hence why many project style "guides" are informal.

[Mario Carneiro]

and my claim is that currently the closest thing we have to "common style" is some amalgam of lean4 core, std, and mathlib styles

[Mac Malone]

Mario Carneiro said:

plus there is value in having code look similar across projects

While true, I think the freedom to code as works best for the developer(s) is more valuable.

[Mac Malone]

Which, I should note, even the professional mathematicians agree with, given there strong opinions on unicode vs ASCII art and other forms of notation.

[Mario Carneiro]

of course you can write code however you like, but not everyone wants to be divergent, and it is helpful to be able to tell people what not being divergent looks like

[Mac Malone]

True, so they should conform with the style of whatever project they admire / aspire to emulate.

[Mac Malone]

I am not really sure what the debate is here.

[Mario Carneiro]

the original claim was that default files is not "common style", it is "lean4 project style"

[Mario Carneiro]

and you were conflating the two

[Mac Malone]

I said "official", not "common".

[Mario Carneiro]

I still think that's the wrong word, lean4 does not maintain an official style guide so there is no such thing

[Mario Carneiro]

I don't think it ever even claimed to

[Mac Malone]

The word "official" is defined as "of or relating to an office or a post of authority." Leo is the authority on Lean 4, so his style (and to a lesser extent Sebastian's) is the "official" style.

[Mario Carneiro]

no that's not how it works

[Mac Malone]

I guess that is our point of disagreement then?

[Mario Carneiro]

lean4 repo is the compiler, it defines the language itself, it also supplies a formatter which is some approximation to common style but isn't that useful as a style guide outside the broad strokes

[Mario Carneiro]

a lean4 style guide is not a deliverable of the lean4 repo

[Mario Carneiro]

I don't think Leo is interested in being the arbiter of lean4 style

[Mario Carneiro]

He has a personal style, and uses that in his project

[Mac Malone]

You seem to be associating a style with a style guide, which I do not think is necessary.

[Mac Malone]

If you write code, and you have any preference on one way of writing things over another, you have a style.

[Mac Malone]

A style guide is simply a written-down consensus of some body on some (not necessarily complete) rules of style.

[Mac Malone]

At least, that is my view (and a view I would argue fits with the definitions of the words in question).

[Mario Carneiro]

sure, but the written-down part is an important aspect of getting consensus

[Mac Malone]

True. But I am not assuming style needs consensus.

[Mario Carneiro]

without it, it's just an idiolect and varies for every person writing code

[Mac Malone]

True. Though if one adopts another's style (e.g., for contributing to their project), it is no longer and idiolect (as more than one person now uses it)

[Mario Carneiro]

Right now, the most actual development on style matters has occurred in mathlib. Lots of people have a style, but mathlib has talked about it and written more about it and come to a broader consensus than other projects

[Mac Malone]

I am not debating that.

[Mario Carneiro]

most of that development has fed back into lean4 repo when it relates to the formatter, so I don't think lean4 core is in disagreement about it

[Mac Malone]

I obviously do disagree with it at points, but that is fine (especially as I am not a major player in the space).

[Mario Carneiro]

Mac said:

True. Though if one adopts another's style (e.g., for contributing to their project), it is no longer and idiolect (as more than one person now uses it)

You would still need to cooperate or coordinate with them in order to use their style, or try to guess at what the style is based on context. Communication is important for making it more than an idiolect and that's why projects get style guides

[Mac Malone]

Mario Carneiro said:

most of that development has fed back into lean4 repo when it relates to the formatter, so I don't think lean4 core is in disagreement about it

I am not sure Leo and Sebastian really care hat much about the output of the formatter so If e.g. Leo did have disagreements on style, I doubt he would express them unless they were major.

[Mario Carneiro]

exactly, "lean4 style" doesn't matter for core because it isn't autoformatting everything

[Mario Carneiro]

so it uses its own style and has rules about not gratuitously applying style fixes

[Mac Malone]

Okay, we agree?

[Mac Malone]

I am still not sure what you are trying to persuade me of / where we are now disagreeing on facts.

[Mario Carneiro]

that "lean4 style" does not equate to "the style of code found in the lean4 repo" and is actually much closer to "the style of code found in the mathlib4 repo"

[Mario Carneiro]

with the latter being primarily due to the pervasive use of mathport

[Mac Malone]

I think that is just a disagreement in definition. I define (official) "lean4-style" as "the style of the [Lean] code found in the lean4 repo".

[Mac Malone]

I personally do not care how common or rare that style is.

[Mac Malone]

Now, if Leo where to develop his own style guide that differed in parts with the Lean 4 repo, then I would concede that that style guide would then be official "lea4-style". Or, if control of Lean 4 was handed over to a foundation and they made a style guide, I would conceded similarly. To me, the official style of the language is the style promulgated by the person or institution with control of the language.

[Mario Carneiro]

The thing I am talking about by the name "common style" or "official style" is "that style for lean4 projects that we recommend to people starting a project for general use"

[Mario Carneiro]

i.e. the thing that would be relevant to lake

[Mac Malone]

Who is "we" in this context?

[Mario Carneiro]

we the lean4 project + community

[Mac Malone]

In that case, there would need to be a meeting of all said stakeholders to sit down and formulating a style guide through some process. Which has not occurred and which I am not sure will occur as I am not sure Leo is that interested in it.

[Mac Malone]

Nor does it seem particularly necessary.

[Mario Carneiro]

Right, this has been my impression. Leo is not interested in making his style "lean4 style", and I think it would be a mistake to put that kind of responsibility on him

[Mac Malone]

As mathlib is currently the primary source of new users, it makes sense they would follow mathlib style and use its resources. Also, those users are less likely to be interested in general programming, so the need for a general style there is somewhat lacking.

[Mario Carneiro]

I think it is actually not that unreasonable to have all the people / projects mentioned agree on a "common style", especially since it doesn't mean "the style your project must adhere to"

[Mario Carneiro]

and what I'm saying is that mathlib has a working draft for "common style" and if you would like to add your input to counteract some real or imagined mathematician-bias please do so

[Mario Carneiro]

just please stop assuming that it is unsuitable just because there are a lot of mathematician users of mathlib

[Mac Malone]

Mario Carneiro said:

agree on a "common style", especially since it doesn't mean "the style your project must adhere to"

That is a very unique notion of "common". If the stakeholders do not use they style they promulgate, I imagine that would be rather confusing for everyone involved.

[Mario Carneiro]

maybe, that's a separate question to be worked on within the context of that project

[Mario Carneiro]

"default style" is another possible framing

[Mac Malone]

Mario Carneiro said:

just please stop assuming that it is unsuitable just because there are a lot of mathematician users of mathlib

I am not assuming it is unsuitable. I am just asserting I disagree with some of it and I think some of my disagreements would be general CS disagreements, which you have also already pointed out exist. E.g. heavy use of Unicode notation, variables, etc.

[Mario Carneiro]

Is that part of the style guide? I don't think it would be

[Mario Carneiro]

In general I would expect most projects to diverge from the "common style" in some specific points but agree on the rest

[Mac Malone]

Now I am confused. I thought you were saying that mathlib4 style was the common style and that its style included these features?

[Mario Carneiro]

no, that was my example of ways mathlib4 project style differs from "common style"

[Mario Carneiro]

i.e. aspects of mathlib4 design I would not copy into downstream projects

[Mac Malone]

Mario Carneiro said:

"default style" is another possible framing

This is starting to sound like the "if you design a cockpit to fit the average pilot, you've actually design it to fit no one" story.

[Mac Malone]

A style guide that no one actually abides by wholly does not strike me as particularly useful.

[Mario Carneiro]

Those are two mutually incompatible claims, or rather they only support the nihilistic view that style guides are useless

[Mac Malone]

Since upon using a project, I have no clue which bits and pieces that have decide to adopt. Thus, this only seems useful if there is a customizable linter to encode a project's style choices.

[Mario Carneiro]

the default is to use all of it, until you find a suggestion that personally offends your sensibilities and so you don't do that one

[Mac Malone]

Mario Carneiro said:

Or rather they only support the nihilistic view that style guides are useless

Which was kind of my point, style guides are really only useful at a project level (where they are enforced) and for new users who want a gist of what to write.

[Mario Carneiro]

okay, call it a template for making project style guides then

[Mac Malone]

Sure. And I think mathlib's work on that is valuable.

[Mac Malone]

I just think the said template will be more mathematician focused and there is not yet a real need (nor a diverse enough userbase to inform it) to create a more general Lean 4 style guide.

[Mario Carneiro]

and lake should implement that template, insofar as it can make explicit recommendations or show by doing

[Mac Malone]

Why should Lake show by doing more than the Lean 4 core?

[Mario Carneiro]

?? lake is a package manager, it is the one responsible for setting up new projects and orienting people in the right direction

[Mario Carneiro]

so the default style guide is quite important for it

[Mario Carneiro]

although granted, it doesn't exactly write a whole lot of code except the lakefile and hello world project right now

[Mac Malone]

Yes, which should effect the templates it generates, but does not necessarily need to effect the codebase itself. In the same manner as the Lean 4 pretty printer vs the Lean 4 core code.

[Mario Carneiro]

yes, this is emphatically only about the output of the tool, not the codebase itself

[Mario Carneiro]

"show by doing" here meaning that when lake produces lean code it should be code that conforms to the style guide

[Mac Malone]

Oh, I was assuming "show by doing" meant "show by doing" in the codebase as opposed to the "explicit recommendations" meaning outputs.

[Mario Carneiro]

also module / folder hierarchy setups etc

[Mac Malone]

Yeah, which is the point of the template system, to make this possible to setup nicely and customize it to what ever style guides end up existing.

[Mario Carneiro]

I don't think there is a huge need for non-default style templates, that sounds like a backup plan if we can't come to some consensus on the default style

[Mac Malone]

Any changes to math template to make it more convenient to mathlib users is welcome.

[Mac Malone]

I severely doubt we will come to a consensus on default style if Leo and Sebastian already do not agree.

[Mario Carneiro]

Leo has not expressed any opinion on default style

[Mario Carneiro]

you are talking about lean4 project style

[Mac Malone]

He did express his strong opinion on parentheses for if (<- x) (as opposed to if <- x).

[Mario Carneiro]

within the context of code in the lean4 project

[Mac Malone]

I mean if he his enforcing it there, I suspect he would like that to be the default style.

[Mario Carneiro]

that's an unjustified assumption

[Mac Malone]

(which is why I have also adopted it)

[Mario Carneiro]

it is possible to have a style opinion and also not recommend it for everyone

[Mac Malone]

I mean, yes, that is possible, but it is not very likely.

[Mac Malone]

I have yet to hear someone assert that their style opinions would be a bad choice for a default style.

[Mario Carneiro]

for instance you might not feel comfortable having enough information to make a decision on behalf of others

[Mario Carneiro]

less so that it's bad and more that you aren't interested in forcing others to follow you

[Mac Malone]

That does not me you would not prefer it, simply that you are not confident enough to assert it.

[Mario Carneiro]

For example, I love autoImplicit and use it in my code, but I know how to tell when it is doing something bad and others might not feel the same way. So I am okay with mathlib taking a different direction here

[Mac Malone]

However, I think both you and I are generally confident enough to assert our opinions and generally would prefer if others followed them.

[Mario Carneiro]

Some features are more expert-oriented, and I would be more hesitant to use them in a default style than in my style

[Mac Malone]

Sure, I can agree with (and I share your views on autoImplicit).

[Mac Malone]

However, I think points of most contention generally are and will be aesthetic choices (and why I believe bikeshedding is so common).

[Mac Malone]

Individuals notions of aesthetic beauty vary and are generally strongly held.

[Mac Malone]

Which since, iirc you are a Philosophy PhD, you may have observed if you took a course in Aesthetics in undergrad.

[Mario Carneiro]

That's why you have to enter these discussions thinking "what would I recommend to others" and not "what would I use"

[Mario Carneiro]

that helps a lot to lower the heckles

[Mac Malone]

Yes, but when it comes to aesthetics, "what would I recommend to others" usually equals "what would I use".

[Mario Carneiro]

(I was a Math/CS undergrad)

[Mac Malone]

And then you become a philosophy PhD?

[Mario Carneiro]

CMU is weird

[Mac Malone]

Sounds like it! :rofl:

[Mac Malone]

For reference, I double majored in CS and Philosophy, and then when on to a CS PhD as that seemed more useful for future job opportunities.

[Mario Carneiro]

I already gave an example where there is an evidence based reason for general recommendation to differ from personal recommendation, because "I" am not "the average person" (which will hold true for various values of "I")

[Mac Malone]

Yes, but that, importantly, was not an aesthetic choice.

[Mac Malone]

I would qualify autoImplicit as convivence rather than aesthetics.

[Mario Carneiro]

there are non-aesthetic reasons you can give for most aspects of formatting

[Mario Carneiro]

if that's what you are thinking about

[Mac Malone]

When I say aesthetics, I would include character choices, naming, indentation, spacing, parentheses, etc.

[Mario Carneiro]

yes, all of the above

[Mac Malone]

Yes, there exist non-aesthetic rationales for some of them, but those are not often enough to choose a specific value / format out of the available options.

[Mario Carneiro]

I would expect a default style guide to contain some aesthetic opinions, aggregated over many people, but mostly non-aesthetic rationales like readability, consistency, searchability etc

[Mario Carneiro]

together with a hefty amount of historical happenstance

[Mac Malone]

I agree. My argument is simply the "aesthetic opinions" part will invariably end up being essentially by fiat
of whatever the ruling party is (and by that I mean the group with the most sway, not necessarily the one with the most authority if the most authority chooses to delegate to e.g. consensus).

[Mario Carneiro]

well, I think it is usually the "historical happenstance" part that wins, based ultimately on the opinions of the people who got there first

[Mac Malone]

Yes, the "ruling party" of the time.

[Mario Carneiro]

because changing a lot of existing code is hard

[Mac Malone]

Very true.

[Mario Carneiro]

and disruptive

[Mario Carneiro]

so you get projects like lean4 repo which have a cross section of slightly different styles across different times in history

[Mac Malone]

Yep.

[Mario Carneiro]

but ultimately, decisions have to be made, so you get as many people together as you can and make a decision

[Mario Carneiro]

mathlib4 in particular had issues with this because we were rolling out code rapidly and needed someone to make a decision, and there was no one at the helm doing style work

[Mac Malone]

I imagine mathport largely decided a lot of that.

[Mario Carneiro]

yeah but what should mathport do?

[Mac Malone]

Whatever you and Daniel ended up deciding?

[Mario Carneiro]

nope, many aspects were tweaked along the way

[Mac Malone]

Along with probably a bit of outside input when issues came up.

[Mario Carneiro]

mathport is a lot better now but it still can't quite get the naming convention right

[Mario Carneiro]

(in part because the information is literally not available)

[Mac Malone]

Mario Carneiro said:

nope, many aspects were tweaked along the way

The key word here I feel is "tweaked". Mathport was thus the origin of the "default style" which was tweaked by the users as necessary, which is similar to the manner you suggested style guides be used.

[Mario Carneiro]

but it was an iterative process, where mathport names something weirdly, a discussion ensues, and mathport is fixed or the naming convention updated

[Mario Carneiro]

hence "aggregated aesthetic opinions"

[Mac Malone]

Yeah?

[Mario Carneiro]

but yes, the dominant style was based on early conversations ultimately stemming to the decision to move to camel-case names for functions in lean 4, based on some internal microsoft user opinions and there I lose track of the origin

[Mario Carneiro]

for indentation, it's always been 2 space indent in lean as long as I can remember, but the 2 space indent of the body is new in lean 4, and the 4 space indent for the signature was a reaction because of readability issues with the 2 space version

[Mac Malone]

A "historical happenstance" with a very good non-aesthetic post-hoc justification. It makes its much more obvious which things are definitions/algorithms and which things are theorems/notation.

[Mario Carneiro]

indeed

[Mario Carneiro]

It makes its much more obvious which things are definitions/algorithms and which things are theorems/notation.

actually I'm not sure what you mean by this

[Mac Malone]

Though, since Lean ends up using all forms of casing style, there really is not an real debate about which to pick, but rather which to use what for.

[Mario Carneiro]

there were some readability issues with the camel case theorem names, although the aesthetic one was also strong

[Mac Malone]

Mario Carneiro said:

It makes its much more obvious which things are definitions/algorithms and which things are theorems/notation.

actually I'm not sure what you mean by this

Now that definitions use camelCase and theorems use snake_case, it makes it easier in e.g. auto-completion to distinguish between them.

[Mario Carneiro]

The one casing convention we don't use is ALL_CAPS

[Mario Carneiro]

I guess because we don't have statics/constants?

[Mac Malone]

It also helps with mathlib's theorem naming style as it keeps definitions one word so that fooCase_eq_barCase is clearly two single functions wherase foo_case_eq_bar_case could be foo case = bar case.

[Mario Carneiro]

right, that's the readability issue

[Mac Malone]

Mario Carneiro said:

I guess because we don't have statics/constants?

We do have them. But I think it is mostly because constants and functions are not sufficiently distinct in Lean to warrant a naming difference.

[Mario Carneiro]

my favorite example involves the theorems about how map, filter and filter_map interact

[Kyle Miller]

There are a lot of messages here, but I think I read enough to understand the disagreement about "official style." @Mac wants to be able to use the phrase "official style" to refer to the style present in Lean 4 core, using an etymology argument from Leo and Sebastian being in a position of authority, but @Mario Carneiro disagrees with calling this "official style" because (though he doesn't say it directly) the phrase "official style" would imply to anyone who heard it that it's somehow the recommended one. There's also the very good point that mathlib already has put in an incredibly large investment into creating an official style (in both the etymological and common senses) and imposing that style on mathlib.

(I usually find etymology-based arguments to be a mott-and-bailey tactic: you find a definition of a word that's least objectionable, to get people to admit the word as a proper description, but then you silently switch to another meaning. I'd object to calling it an "official style" as well to make sure no one will (un)intentionally use this tactic. If you want, dictionaries themselves are just style guides on what words should mean, to help resolve disagreements.)

[Mac Malone]

Kyle Miller said:

If you want, dictionaries themselves are just style guides on what words should mean, to help resolve disagreements.

This is a funny, but largely apt analogy. :laughing:

[Kyle Miller]

I'm not joking :shrug: But it's amusing

[Mac Malone]

I know, but yeah it is amusing.

[Mac Malone]

Kyle Miller said:

I usually find etymology-based arguments to be a mott-and-bailey tactic: you find a definition of a word that's least objectionable, to get people to admit the word as a proper description, but then you silently switch to another meaning.

I am a strong believer in etymological arguments for word meanings, as I think they are the only thing that can approach a plausible objective "correct" notion of what a word should mean. However, I do concede that they can also be easily manipulated to achieve a desired result through selective rhetoric.

[Kyle Miller]

Meaning is a negotiation between multiple parties, and meanings of individual words are part of that negotiation. In a public discussion like this, we're negotiating whether "official" should apply in this context in this discussion in this community. Using an etymological argument is one sort of argument to support a meaning, and it can seem like it's more objective, but it's in the end still a style/aesthetic/practical argument for using some words to refer to some concept, to try to justify that the words won't refer to some other concept.

[Kyle Miller]

Don't get me wrong, I like etymologies a lot, and https://www.etymonline.com/ is one of the websites I most frequently visit.

[Kyle Miller]

I see it mostly as a way to understand how words could possibly have obtained the meanings that they do, rather than trying to undertake some project to restore true meanings of words.

[Mac Malone]

Kyle Miller said:

Meaning is a negotiation between multiple parties, and meanings of individual words are part of that negotiation. In a public discussion like this, we're negotiating whether "official" should apply in this context in this discussion in this community.

Personally, I disagree with this notion of meaning, which I interpret to be akin to Wittgenstein's use theory.

[Kyle Miller]

I'm saying something different I think, which is that meaning takes active maintenance. We can't be certain we've meant anything to anyone unless we put in effort to check.

Fierce debates about meanings of words are a good thing (it's putting energy into making sure we can be more certain we will be understood). I think it should be thought of as being like working on an API boundary for a network protocol, which can be implemented in clients any number of ways. Getting everyone synchronized can take a whole lot of effort and political will.

Regarding "official", it's had the additional meaning "authorized by authority" since at least 1854, so I expect it to be a whole lot of work to get it to once again unambiguously mean "of or relating to an office or post of authority", even to just this Zulip.

[Mac Malone]

Kyle Miller said:

I'm saying something different I think, which is that meaning takes active maintenance. We can't be certain we've meant anything to anyone unless we put in effort to check.

That I mostly agree with.

Kyle Miller said:

Regarding "official", it's had the additional meaning "authorized by authority" since at least 1854, so I expect it to be a whole lot of work to get it to once again unambiguously mean "of or relating to an office or post of authority", even to just this Zulip.

Fair enough, but even in that case, there simply would not be an "official style", as Leo has yet to authorize one (afaik). Though, I imagine there could by a secondary debate on who qualifies as a Lean "authority".