search

nikomatsakis / rust-design-axioms

Discovering and describing Rust's design axioms
https://nikomatsakis.github.io/rust-design-axioms/
Other
66 stars 3 forks source link

Consider expanding a bit more about the nature of the axioms #13

Open grodin opened 9 months ago

grodin commented 9 months ago

It may be worth clarifying more the intention of these axioms. I found myself thinking about whether the current set of axioms is minimal (are some consequences of others?) and independence of the axioms (which you seem to be considering in e.g. #3).

I realised that I don't know whether these questions are even relevant, and to what extent. It may be worth clarifying things along these lines (or maybe it's worth leaving up in the air, to be clarified as the axioms are developed).

I think that this project is very valuable and reflects to me something very appealing about rust: the willingness of core rustaceans to both develop the principles underlying rust in the open, and to return to those principles to clarify/reconsider them.

nikomatsakis commented 9 months ago

@grodin good questions. I'm thinking about it! I think my opinion is that first and foremost they should be useful, as in, we should be able to apply them to active debates and move those debates forward. I think independence and minimality are important to the extent that they serve that ultimate goal. Independence seems important for ordering: if there's overlap, then which do you prefer? Typically non-independent axioms could, I think, be refined into something more precise.

Minimality is a bit hard to define. The thing I am also curious about is "complete" -- do they have to cover all aspects of Rust? I suspect the answer is that they could not, but that they strive to cover the most important.

grodin commented 9 months ago

Minimal there refers to the set of axioms. The question I had in mind was: "is this is the smallest set of axioms that says what I want it to?" There's a big overlap between minimality and independence.

Minimality is quite valuable for the axioms for a formal theory; it's probably much less so here where it's not about strict logical consequences but more about understandability and communicability.

It's probably just my own background: when I see the word axiom I start thinking like a mathematician!

grodin commented 9 months ago

Minimal there refers to the set of axioms. The question I had in mind was: "is this is the smallest set of axioms that says what I want it to?" There's a big overlap between minimality and independence.

Minimality is quite valuable for the axioms for a formal theory; it's probably much less so here where it's not about strict logical consequences but more about understandability and communicability.

It's probably just my own background: when I see the word axiom I start thinking like a mathematician!