[deltasepsilon]

I think the importance of this work is best illustrated by a simple example [1]. If that link doesn't work, go to https://cerberus.cl.cam.ac.uk/ select File->Popl 2019 and pick the second example (basic_local_yx) and run the sim (hit forward). The experimental data is interesting, specifically that from CompCert. This project allows work towards a certified optimizing compiler, assuming you can decide on a semantics.

Also, as I said on this item [2], Rust is no panacea. It's hard to argue this, since the overwhelming majority of programmers on HN are well and truly mentally oblivious due to poor education, but if your programming language does not have a semantics you cannot even begin to ask if your code is correct because the question itself doesn't make any sense. I am so exhausted at this state of affairs.

[1] https://cerberus.cl.cam.ac.uk/#%7B%220%22%3A%7B%221%22%3A%22...

[2] https://news.ycombinator.com/item?id=33096395

[littlestymaar]

> Also, as I said on this item [2], Rust is no panacea. […], but if your programming language does not have a semantics you cannot even begin to ask if your code is correct because the question itself doesn't make any sense.

AFAIK safe Rust is OK, but that's true that unsafe Rust has been pretty much “whatever LLVM will do with the IR that rustc generates”, but properly formalizing the semantic has been ongoing for years and has already started to give actionable results. The current state of things is still far from optimal, but at the same time you're always going to have an implementation of your programming language before you have a formal semantic, because nobody is ever going to use a language with a semantic but no implementation…

[deltasepsilon]

> nobody is ever going to use a language with a semantic but no implementation

I appreciate what you're saying, however, hear me out. Suppose we had a language with a defined semantics and a useable implementation. We could use that language to implement, say Rust, and in so doing have a semantics for Rust, a semantics defined by its implementation. The point is, to be principled, we have to start somewhere. Make that language basic so that we are capable of providing a semantics. Now, granted, the "semantics" we generate for Rust in doing so will be necessarily pessimistic, i.e. overly determined. But then one could develop tooling to "prune" the implementation defined semantics somehow towards an idealized semantics. I don't think anyone has seriously pursued this avenue of thought.

Also, I must add, I appreciate your thoughtful elision from my quote. I need to stop getting worked up. But truly, software feels like it's perpetually in the dark ages. We have such incredible compute power thanks to the tireless effort of hardware engineers, and still we're programming with the equivalent of "stone knives and bear skins".

[tialaramex]

As I understand it, the larger purpose of this work is as part of efforts to persuade WG14 to pick actual provenance semantics, presumably a PNVI-ae variant. As just a TR, the same as with the original thesis, it doesn't do anything.

Whereas with Rust the point is to actually do something, including in this particular case Aria's Strict Provenance Experiment, which is basically "What if Rust insisted on full blown PNVI?". Obviously the answer is "Well that can't work" but like, how much. How much can't it work? Hence the experiment.

[pjmlp]

I doubt they would get persuaded, as much as they have been into anything related to improving C's safety.

[jcranmer]

From what I understand, the C committee is very interested in adopting pointer provenance semantics, but they also tend to operate at the speed of molasses and this is of course a research-hard problem.

[pjmlp]

Well, in 50 years they have hardly bothered to add any kind of fat pointer as suggested by Dennis Ritchie, Walter Bright and others, struct based vocabulary types for string and arrays, annotations like SAL.

Hence why I hardly believe pointer provenance is going to be any different.

[tialaramex]

Last I looked WG14 intended to knock together a TS for provenance in the C23 timeframe (so, this year). Of course a TS might go nowhere, vendors could ignore it, it might be a dead end, but I don't believe WG14 produced a TS of sane array types, or fat pointers.

[nullifidian]

People are working on the formal specification of rust. It isn't easy. There are at least three projects, maybe more if we include academia https://github.com/RalfJung/minirust has a summary of efforts in the end of the readme.

the basics of the rust typesystem were proven correct for a restricted rust subset in the rustbelt project.