RFC: introduce notations for Duration and Timestamp and remove dangerous OfNat instances

[TwoFX]

Proposal

We currently provide OfNat Duration and OfNat Timestamp instances which turn natural numbers into seconds and seconds since Unix epoch, respectively. Keeping with the design of "make incorrect conversions impossible and make dubious conversions explicit", we should change this as follows:

• Introduce notation for Duration types (this was considered during initial implementation, but was postponed to reduce the size of the PR).
• Add Timestamp.ofDurationSinceUnixEpoch (this is just the constructor).
• Remove the OfNat Duration and OfNat Timestamp instances.
• Possibly introduce notation for Timestamp that allows entering a timestamp with time zone in ISO format without having to go through ZonedDateTime.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[lambda-fairy]

Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Concern.20with.20.60instance.20OfNat.20Timestamp.60.20.28and.20.60Duration.60.29

[lambda-fairy]

I wonder if it's worth making the constructor of Timestamp harder to access as well. (With protected?)

Semantically, Timestamp is a physical point in time. The fact that it's an offset from Jan 1, 1970 is an implementation detail and should be hidden.

For reference, Rust enforces that semantic boundary strictly, such that getting the Unix epoch offset requires subtraction: timestamp.duration_since(UNIX_EPOCH). (I'm not suggesting we need to go that far – just offering a data point.)