IDL spec: Remove unsound rules

[nomeata]

now that other teams are starting to look at the IDL spec we should not
confuse them by having broken rules in this document, so let’s remove
them.

Issue #364 is where we are discussing possible ways to fix them.

[nomeata]

@rossberg ping?

[rossberg]

Is there much risk of confusion? The disclaimer seems explicit enough.

Not too big a fan of creating more churn than necessary. Something close to these rules still is what we want, isn't it?

[nomeata]

Something close to these rules still is what we want, isn't it?

We just had a multip day discussion about this without a conclusion. I think pretending we know what we want in the end at this point is not honest. And I found it mildly confusing when scrolling through while doing the Coq proofs.

Just like I usually ask people to remove commented out “not yet working” code, why not apply the same to specifications? It’s not lost, if we really end up needing it, and a git revert or git show + copy’n’paste is cheap. It will also make reviewing an eventual PR adding this properly easier to understand.

[nomeata]

@rossberg ping? I am still in favor of keeping the IDL spec that we are already handing out to other team for implementation free of broken stuff.

[rossberg]

Meant to look into it this week, preferably, by fixing it instead of removing. :)

[nomeata]

Ok. I will remove them at the end of the week if we have nothing fixed by then :-)

[nomeata]

(hopefully superceded by #832)

[nomeata]

Ok. I will remove them at the end of the week if we have nothing fixed by then :-)

It’s been more than a week. Can we just satisfy my OCD and not leave broken stuff around? I promise to merge master into #832 and handle the conflict :-)

[rossberg]

I don't think it's a problem to keep todos around, to the contrary, as long as they are clearly marked as such. But if you feel strongly about it, go ahead.

[rossberg]

Instead of removing altogether, replace them with shorter TODOs to clarify that something is still missing.

[nomeata]

Instead of removing altogether, replace them with shorter TODOs to clarify that something is still missing.

Very good idea, done!