Stream: project-ffi-unwind

Topic: tbd vs ub vs unspecified behavior


view this post on Zulip nikomatsakis (Oct 16 2019 at 10:05):

I've prepared a pull request that refines the terminology along the lines we discussed yesterday. In particular, it separates

view this post on Zulip nikomatsakis (Oct 16 2019 at 10:05):

Comments welcome.

view this post on Zulip nikomatsakis (Oct 16 2019 at 10:06):

@gnzlbg, does that address your confusion?

view this post on Zulip gnzlbg (Oct 16 2019 at 11:55):

Yes. I think that matches how I worded my thoughts in the other PR, where UB is mostly only used for "there is no reasonable way in which we could define the behavior here or no useful guarantees that we could provide"

view this post on Zulip BatmanAoD (Kyle Strand) (Oct 16 2019 at 16:38):

Thanks very much for doing this. I have been thinking that introducing some terminology as a standard for the Rust project overall would be worth its own RFC, but in the mean time this WG can adopt it for our own purposes, as long as we're explicit about it

view this post on Zulip BatmanAoD (Kyle Strand) (Oct 16 2019 at 16:38):

only gave a cursory look to the PR so far but I think it seems good

view this post on Zulip nikomatsakis (Oct 17 2019 at 16:19):

@gnzlbg regarding our discussion on https://github.com/nikomatsakis/project-ffi-unwind/pull/10, I tried to summarize the situation and all relevant facts in a hackmd document -- I'm curious if you feel there are points missing or points that you disagree with in there.

view this post on Zulip gnzlbg (Oct 17 2019 at 16:32):

So I think that captures most of it

view this post on Zulip gnzlbg (Oct 17 2019 at 16:32):

In the section about whether TBD should hit stable, I'd word it a bit differently

view this post on Zulip gnzlbg (Oct 17 2019 at 16:32):

All unspecified behavior hits stable, that's normal

view this post on Zulip gnzlbg (Oct 17 2019 at 16:33):

I don't think it is worth it to introduce a definition for TBD in the rust language reference

view this post on Zulip gnzlbg (Oct 17 2019 at 16:33):

I think it would suffice to say "unspecified behavior" and maybe have a note saying "we are trying to specify this here (link)"

view this post on Zulip gnzlbg (Oct 17 2019 at 16:34):

When it comes to unspecified behavior, we have all sorts of notes everywhere anyways documenting how certain platforms work

view this post on Zulip gnzlbg (Oct 17 2019 at 16:35):

For me personally, it would be useful to be able to tell when reading a document that should turn into an RFC at some point, which parts of the document are unspecified because we intend the feature to hit stable in that way, and which parts are unspecified because we haven't looked at it yet

view this post on Zulip nikomatsakis (Oct 17 2019 at 16:37):

I don't think it is worth it to introduce a definition for TBD in the rust language reference

(I didn't intend to either)

view this post on Zulip nikomatsakis (Oct 17 2019 at 16:37):

I think it would suffice to say "unspecified behavior" and maybe have a note saying "we are trying to specify this here (link)"

exactly what I had in mind

view this post on Zulip gnzlbg (Oct 17 2019 at 16:38):

For users on stable Rust that have to use such unspecified behavior, it is obviously useful as well to know which unspecified behavior is intended to be unspecified long term, and which is being worked on, so it would be nice to have a way to hint at this as well

view this post on Zulip gnzlbg (Oct 17 2019 at 16:38):

exactly what I had in mind

So I think we agree. The document looks fine to me.

view this post on Zulip nikomatsakis (Oct 17 2019 at 16:40):

great.

view this post on Zulip nikomatsakis (Oct 17 2019 at 16:40):

I updated it a bit to clarify the points you raised

view this post on Zulip gnzlbg (Oct 17 2019 at 16:43):

I've added an answer to the question about stable Rust code using this already

view this post on Zulip gnzlbg (Oct 17 2019 at 16:43):

We have had nightly features to avoid UB for a while, and for different reasons, users have not been able to use them

view this post on Zulip nikomatsakis (Oct 17 2019 at 17:03):

I've added an answer to the question about stable Rust code using this already

good point!

view this post on Zulip nikomatsakis (Oct 17 2019 at 17:03):

BTW, @gnzlbg, I can't entirely tell if this concern is still relevant

view this post on Zulip gnzlbg (Oct 17 2019 at 17:04):

No it isn't, has been resolved

view this post on Zulip gnzlbg (Oct 17 2019 at 17:04):

For some reason I cannot resolve it :/

view this post on Zulip gnzlbg (Oct 17 2019 at 17:04):

The button does not show

view this post on Zulip nikomatsakis (Oct 17 2019 at 17:05):

oh probably because you don't have write access or something to the repo

view this post on Zulip nikomatsakis (Oct 17 2019 at 17:05):

I should transfer this to rust-lang

view this post on Zulip gnzlbg (Oct 17 2019 at 17:05):

Ah ok, that makes sense, please resolve it for me

view this post on Zulip nikomatsakis (Oct 17 2019 at 17:05):

I was kind of waiting but .. that's sort of silly

view this post on Zulip nikomatsakis (Oct 17 2019 at 17:13):

OK, I revised some of the text and added that hackmd to the repo as our first "resolved concern" and I pushed some other improvements. Going to merg.

view this post on Zulip BatmanAoD (Kyle Strand) (Oct 17 2019 at 18:04):

Once again I submitted a review post-merge...not sure how inconvenient that is as a form of communication.

view this post on Zulip BatmanAoD (Kyle Strand) (Oct 25 2019 at 09:51):

How is "unsoundness" defined? Is it potentially a better term than "LLVM-UB" for things that are known to be unsafe?

view this post on Zulip gnzlbg (Oct 25 2019 at 09:59):

The UCG reference has a definition for that

view this post on Zulip gnzlbg (Oct 25 2019 at 10:00):

https://github.com/rust-lang/unsafe-code-guidelines/blob/master/reference/src/glossary.md#soundness-of-code--of-a-library

view this post on Zulip gnzlbg (Oct 25 2019 at 10:01):

"sound == well-typed programs cannot cause Undefined Behavior"

view this post on Zulip centril (Oct 25 2019 at 10:01):

A safe function is unsound if for some inputs or program states it can lead to a trace that has UB.

view this post on Zulip gnzlbg (Oct 25 2019 at 10:02):

@Kyle Strand since sound is defined in terms of UB, i don't think you can replace "LLVM-UB" with it (EDIT: unless I'm misunderstanding which use of LLVM-UB you are talking about)

view this post on Zulip centril (Oct 25 2019 at 10:02):

@Kyle Strand https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/ is a good read

view this post on Zulip gnzlbg (Oct 25 2019 at 10:04):

Probably not the best introduction if you haven't used the term before


Last updated: Jan 26 2022 at 08:34 UTC