Topic: [std-proposals] Re: Enforcing safe coding techniques
Author: Nicol Bolas <jmckesson@gmail.com>
Date: Tue, 13 Mar 2018 19:51:36 -0700 (PDT)
Raw View
------=_Part_4001_1572353424.1520995896437
Content-Type: multipart/alternative;
boundary="----=_Part_4002_1590594207.1520995896437"
------=_Part_4002_1590594207.1520995896437
Content-Type: text/plain; charset="UTF-8"
Consider this:
struct S
{
shared_ptr<S> ptr;
int val;
};
auto ptr1 = make_shared<S>(nullptr, 4);
auto ptr2 = make_shared<S>(ptr1, 6);
auto ptr3 = make_shared<S>(ptr2, -3);
ptr1.ptr = ptr3;
Ignore the fact that `make_shared` doesn't work with aggregates. Can you
provide a simple rule which would let the compiler decide that this code is
"unsafe"? What if each of those pointer creation and assignment functions
were hidden behind several layers of functions, so that the compiler can't
see everything?
Just because all individual parts are "safe" doesn't mean that the whole
is. And if you're going to define a subset of C++ that you consider "safe",
it had better *actually be safe*. The last thing C++ programmers need is
having language features that give them a false sense of security about how
"safe" their code is.
Now consider this:
int arr[3] = {5, 2, -13};
arr[1] = 6;
This is perfectly, 100% functional code. Given everything we can see here,
there is zero chance of UB or other such. Would this be considered "safe"
code? And if not, why not?
From your description of the actions you want to consider "unsafe", what
you really mean is "low-level" or "not-modern". Neither is genuinely
"safe"; it may be "safe*r*", but that's a lot different from "safe".
And that sort of thing is far better left up to each individual programmer
and their static analysis tools of choice.
--
You received this message because you are subscribed to the Google Groups "ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an email to std-proposals+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
To view this discussion on the web visit https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/1a250082-a1d8-4f36-93a3-8540056ff279%40isocpp.org.
------=_Part_4002_1590594207.1520995896437
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr">Consider this:<br><br><div style=3D"background-color: rgb(=
250, 250, 250); border-color: rgb(187, 187, 187); border-style: solid; bord=
er-width: 1px; overflow-wrap: break-word;" class=3D"prettyprint"><code clas=
s=3D"prettyprint"><div class=3D"subprettyprint"><span style=3D"color: #008;=
" class=3D"styled-by-prettify">struct</span><span style=3D"color: #000;" cl=
ass=3D"styled-by-prettify"> S<br></span><span style=3D"color: #660;" class=
=3D"styled-by-prettify">{</span><span style=3D"color: #000;" class=3D"style=
d-by-prettify"><br>=C2=A0 shared_ptr</span><span style=3D"color: #660;" cla=
ss=3D"styled-by-prettify"><</span><span style=3D"color: #000;" class=3D"=
styled-by-prettify">S</span><span style=3D"color: #660;" class=3D"styled-by=
-prettify">></span><span style=3D"color: #000;" class=3D"styled-by-prett=
ify"> ptr</span><span style=3D"color: #660;" class=3D"styled-by-prettify">;=
</span><span style=3D"color: #000;" class=3D"styled-by-prettify"><br>=C2=A0=
</span><span style=3D"color: #008;" class=3D"styled-by-prettify">int</span=
><span style=3D"color: #000;" class=3D"styled-by-prettify"> val</span><span=
style=3D"color: #660;" class=3D"styled-by-prettify">;</span><span style=3D=
"color: #000;" class=3D"styled-by-prettify"><br></span><span style=3D"color=
: #660;" class=3D"styled-by-prettify">};</span><span style=3D"color: #000;"=
class=3D"styled-by-prettify"><br><br></span><span style=3D"color: #008;" c=
lass=3D"styled-by-prettify">auto</span><span style=3D"color: #000;" class=
=3D"styled-by-prettify"> ptr1 </span><span style=3D"color: #660;" class=3D"=
styled-by-prettify">=3D</span><span style=3D"color: #000;" class=3D"styled-=
by-prettify"> make_shared</span><span style=3D"color: #660;" class=3D"style=
d-by-prettify"><</span><span style=3D"color: #000;" class=3D"styled-by-p=
rettify">S</span><span style=3D"color: #660;" class=3D"styled-by-prettify">=
>(</span><span style=3D"color: #008;" class=3D"styled-by-prettify">nullp=
tr</span><span style=3D"color: #660;" class=3D"styled-by-prettify">,</span>=
<span style=3D"color: #000;" class=3D"styled-by-prettify"> </span><span sty=
le=3D"color: #066;" class=3D"styled-by-prettify">4</span><span style=3D"col=
or: #660;" class=3D"styled-by-prettify">);</span><span style=3D"color: #000=
;" class=3D"styled-by-prettify"><br></span><span style=3D"color: #008;" cla=
ss=3D"styled-by-prettify">auto</span><span style=3D"color: #000;" class=3D"=
styled-by-prettify"> ptr2 </span><span style=3D"color: #660;" class=3D"styl=
ed-by-prettify">=3D</span><span style=3D"color: #000;" class=3D"styled-by-p=
rettify"> make_shared</span><span style=3D"color: #660;" class=3D"styled-by=
-prettify"><</span><span style=3D"color: #000;" class=3D"styled-by-prett=
ify">S</span><span style=3D"color: #660;" class=3D"styled-by-prettify">>=
(</span><span style=3D"color: #000;" class=3D"styled-by-prettify">ptr1</spa=
n><span style=3D"color: #660;" class=3D"styled-by-prettify">,</span><span s=
tyle=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=3D"c=
olor: #066;" class=3D"styled-by-prettify">6</span><span style=3D"color: #66=
0;" class=3D"styled-by-prettify">);</span><span style=3D"color: #000;" clas=
s=3D"styled-by-prettify"><br></span><span style=3D"color: #008;" class=3D"s=
tyled-by-prettify">auto</span><span style=3D"color: #000;" class=3D"styled-=
by-prettify"> ptr3 </span><span style=3D"color: #660;" class=3D"styled-by-p=
rettify">=3D</span><span style=3D"color: #000;" class=3D"styled-by-prettify=
"> make_shared</span><span style=3D"color: #660;" class=3D"styled-by-pretti=
fy"><</span><span style=3D"color: #000;" class=3D"styled-by-prettify">S<=
/span><span style=3D"color: #660;" class=3D"styled-by-prettify">>(</span=
><span style=3D"color: #000;" class=3D"styled-by-prettify">ptr2</span><span=
style=3D"color: #660;" class=3D"styled-by-prettify">,</span><span style=3D=
"color: #000;" class=3D"styled-by-prettify"> </span><span style=3D"color: #=
660;" class=3D"styled-by-prettify">-</span><span style=3D"color: #066;" cla=
ss=3D"styled-by-prettify">3</span><span style=3D"color: #660;" class=3D"sty=
led-by-prettify">);</span><span style=3D"color: #000;" class=3D"styled-by-p=
rettify"><br>ptr1</span><span style=3D"color: #660;" class=3D"styled-by-pre=
ttify">.</span><span style=3D"color: #000;" class=3D"styled-by-prettify">pt=
r </span><span style=3D"color: #660;" class=3D"styled-by-prettify">=3D</spa=
n><span style=3D"color: #000;" class=3D"styled-by-prettify"> ptr3</span><sp=
an style=3D"color: #660;" class=3D"styled-by-prettify">;</span><span style=
=3D"color: #000;" class=3D"styled-by-prettify"><br></span></div></code></di=
v><br>Ignore the fact that `make_shared` doesn't work with aggregates. =
Can you provide a simple rule which would let the compiler decide that this=
code is "unsafe"? What if each of those pointer creation and ass=
ignment functions were hidden behind several layers of functions, so that t=
he compiler can't see everything?<br><br>Just because all individual pa=
rts are "safe" doesn't mean that the whole is. And if you'=
;re going to define a subset of C++ that you consider "safe", it =
had better <i>actually be safe</i>. The last thing C++ programmers need is =
having language features that=20
give them a false sense of security about how "safe" their code i=
s.<br><br>Now consider this:<br><br><div style=3D"background-color: rgb(250=
, 250, 250); border-color: rgb(187, 187, 187); border-style: solid; border-=
width: 1px; overflow-wrap: break-word;" class=3D"prettyprint"><code class=
=3D"prettyprint"><div class=3D"subprettyprint"><span style=3D"color: #008;"=
class=3D"styled-by-prettify">int</span><span style=3D"color: #000;" class=
=3D"styled-by-prettify"> arr</span><span style=3D"color: #660;" class=3D"st=
yled-by-prettify">[</span><span style=3D"color: #066;" class=3D"styled-by-p=
rettify">3</span><span style=3D"color: #660;" class=3D"styled-by-prettify">=
]</span><span style=3D"color: #000;" class=3D"styled-by-prettify"> </span><=
span style=3D"color: #660;" class=3D"styled-by-prettify">=3D</span><span st=
yle=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=3D"co=
lor: #660;" class=3D"styled-by-prettify">{</span><span style=3D"color: #066=
;" class=3D"styled-by-prettify">5</span><span style=3D"color: #660;" class=
=3D"styled-by-prettify">,</span><span style=3D"color: #000;" class=3D"style=
d-by-prettify"> </span><span style=3D"color: #066;" class=3D"styled-by-pret=
tify">2</span><span style=3D"color: #660;" class=3D"styled-by-prettify">,</=
span><span style=3D"color: #000;" class=3D"styled-by-prettify"> </span><spa=
n style=3D"color: #660;" class=3D"styled-by-prettify">-</span><span style=
=3D"color: #066;" class=3D"styled-by-prettify">13</span><span style=3D"colo=
r: #660;" class=3D"styled-by-prettify">};</span><span style=3D"color: #000;=
" class=3D"styled-by-prettify"><br>arr</span><span style=3D"color: #660;" c=
lass=3D"styled-by-prettify">[</span><span style=3D"color: #066;" class=3D"s=
tyled-by-prettify">1</span><span style=3D"color: #660;" class=3D"styled-by-=
prettify">]</span><span style=3D"color: #000;" class=3D"styled-by-prettify"=
> </span><span style=3D"color: #660;" class=3D"styled-by-prettify">=3D</spa=
n><span style=3D"color: #000;" class=3D"styled-by-prettify"> </span><span s=
tyle=3D"color: #066;" class=3D"styled-by-prettify">6</span><span style=3D"c=
olor: #660;" class=3D"styled-by-prettify">;</span><span style=3D"color: #00=
0;" class=3D"styled-by-prettify"><br></span></div></code></div><br>This is =
perfectly, 100% functional code. Given everything we can see here, there is=
zero chance of UB or other such. Would this be considered "safe"=
code? And if not, why not?<br><br>From your description of the actions you=
want to consider "unsafe", what you really mean is "low-lev=
el" or "not-modern". Neither is genuinely "safe"; =
it may be "safe<u><i><b>r</b></i></u>", but that's a lot diff=
erent from "safe".<br><br>And that sort of thing is far better le=
ft up to each individual programmer and their static analysis tools of choi=
ce.<br></div>
<p></p>
-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals" group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/1a250082-a1d8-4f36-93a3-8540056ff279%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/1a250082-a1d8-4f36-93a3-8540056ff279=
%40isocpp.org</a>.<br />
------=_Part_4002_1590594207.1520995896437--
------=_Part_4001_1572353424.1520995896437--
.
Author: Arthur O'Dwyer <arthur.j.odwyer@gmail.com>
Date: Thu, 15 Mar 2018 13:36:14 -0700 (PDT)
Raw View
------=_Part_922_2039975677.1521146174697
Content-Type: multipart/alternative;
boundary="----=_Part_923_870154088.1521146174698"
------=_Part_923_870154088.1521146174698
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
On Tuesday, March 13, 2018 at 4:32:51 PM UTC-7, Mikl=C3=B3s P=C3=A1l wrote:
>
> Proposed qualifiers:=20
>
> =E2=80=9Csafe=E2=80=9D: qualifies functions, where unsafe coding techniqu=
es are not=20
> allowed by the compiler.
>
> =E2=80=9Ctrusted=E2=80=9D: qualifies functions, where unsafe coding techn=
iques are=20
> allowed, but their correctness is proven by the author.
>
> Unqualified code: functions, where unsafe coding techniques are allowed,=
=20
> and their correctness is unknown.
>
This idea is very similar to Rust in theory. But in practice, in C++, I=20
guess I don't see why you need these qualifiers at all.
In the definition of "trusted"-qualified code, you say that the correctness=
=20
of trusted code must be "proven". If this means an informal, math-style=20
paper proof, then there is no difference in practice between "trusted" and=
=20
"unqualified" code =E2=80=94 both of them are formally unproven and unsafe,=
with=20
some human being standing outside the computer going "hey, trust me, I=20
write good code."
So let's assume that by "proven" you mean in the formal program-proof=20
sense: "trusted" code may use unsafe constructs, but it carries a program=
=20
proof of its correctness, using annotations essentially like the Contracts=
=20
proposals coming from people like Lisa Lippincott. The compiler (or some=20
compiler-like tool) can read these annotations and check them for=20
correctness-of-proof.
So then in the definition of "safe"-qualified code, you say that the=20
compiler should disallow "unsafe" coding techniques. The only meaning I can=
=20
assign to the word "unsafe" here is "coding techniques that (might) lead to=
=20
program-incorrectness." So, in "safe"-qualified code, the compiler will be=
=20
checking that the code is provably correct. In other words, there is no=20
difference between "safe"-qualified code and "trusted"-qualified code,=20
except that in "safe" code we expect to write fewer annotations. (But=20
certainly we can't write *no* annotations =E2=80=94 since the compiler is t=
o check=20
the correctness of our code, we still need to tell the compiler what it=20
*means* to be correct! That is, we must annotate our "safe"-qualified code=
=20
with preconditions and postconditions anyway.)
So at this point we have two kinds of code:
- Code with "sufficiently many" annotations, where the tool is supposed to=
=20
check our work. Safe code has few annotations; trusted code has more=20
annotations.
- Code with no annotations, where we admit that we are doing unsafe things=
=20
(and suppressing the tool) but promise that it's okay.
(And of course there might be some code with "insufficiently many"=20
annotations, which will be rejected by the tool.)
This sounds like it could all be done with something as simple as "#pragma=
=20
checking on" and "#pragma checking off" (say, at function granularity).
I don't think it requires or even suggests any *core language* changes.
It seems to me that the hard work here (which, again, at least some of=20
which is being done by the Contracts people) is in designing the=20
proof-checking tool and in designing the annotation syntax that allows us=
=20
to communicate our invariants to the tool (e.g. the syntax of the operands=
=20
to [[expects:]] and [[ensures:]]).
=E2=80=93Arthur
P.S. =E2=80=94 If there is a flaw in my argument, I think it is that I am c=
ombining=20
both "undesired behavior" and "undefined behavior" under the single rubric=
=20
of "program incorrectness." I think Rust's "safe" corresponds not to=20
"provably correct" but merely "provably *not undefined behavior*" (i.e.=20
each function's precondition is merely "UB has not yet occurred" and its=20
postcondition is "UB has still not occurred"). Unfortunately I can't see=20
how to achieve "provably *not undefined behavior*" in C++ given the=20
existence of multithreading and non-owning references.
>
--=20
You received this message because you are subscribed to the Google Groups "=
ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to std-proposals+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
To view this discussion on the web visit https://groups.google.com/a/isocpp=
..org/d/msgid/std-proposals/85942f26-7a66-4543-9a38-d46a1bdf6cb3%40isocpp.or=
g.
------=_Part_923_870154088.1521146174698
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr">On Tuesday, March 13, 2018 at 4:32:51 PM UTC-7, Mikl=C3=B3=
s P=C3=A1l wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0;margi=
n-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"l=
tr">
<h1><span style=3D"font-size: 13px;">Proposed
qualifiers:</span></h1>
<p class=3D"MsoNormal"><span lang=3D"EN-US">=E2=80=9Csafe=E2=80=9D:
qualifies functions, where unsafe coding techniques are not allowed by the
compiler.</span></p>
<p class=3D"MsoNormal"><span lang=3D"EN-US">=E2=80=9Ctrusted=E2=80=9D:
qualifies functions, where unsafe coding techniques are allowed, but their
correctness is proven by the author.</span></p>
<p class=3D"MsoNormal"><span lang=3D"EN-US">Unqualified
code: functions, where unsafe coding techniques are allowed, and their
correctness is unknown.</span></p></div></blockquote><div><br></div><div>Th=
is idea is very similar to Rust in theory. But in practice, in C++, I guess=
I don't see why you need these qualifiers at all.</div><div><br></div>=
<div>In the definition of "trusted"-qualified code, you say that =
the correctness of trusted code must be "proven". If this means a=
n informal, math-style paper proof, then there is no difference in practice=
between "trusted" and "unqualified" code =E2=80=94 bot=
h of them are formally unproven and unsafe, with some human being standing =
outside the computer going "hey, trust me, I write good code."</d=
iv><div>So let's assume that by "proven" you mean in the form=
al program-proof sense: "trusted" code may use unsafe constructs,=
but it carries a program proof of its correctness, using annotations essen=
tially like the Contracts proposals coming from people like Lisa Lippincott=
.. The compiler (or some compiler-like tool) can read these annotations and =
check them for correctness-of-proof.</div><div><br></div><div>So then in th=
e definition of "safe"-qualified code, you say that the compiler =
should disallow "unsafe" coding techniques. The only meaning I ca=
n assign to the word "unsafe" here is "coding techniques tha=
t (might) lead to program-incorrectness." So, in "safe"-qual=
ified code, the compiler will be checking that the code is provably correct=
.. In other words, there is no difference between "safe"-qualified=
code and "trusted"-qualified code, except that in "safe&quo=
t; code we expect to write fewer annotations. (But certainly we can't w=
rite <i>no</i> annotations =E2=80=94 since the compiler is to check the cor=
rectness of our code, we still need to tell the compiler what it <i>means</=
i> to be correct! That is, we must annotate our "safe"-qualified =
code with preconditions and postconditions anyway.)</div><div><br></div><di=
v>So at this point we have two kinds of code:</div><div>- Code with "s=
ufficiently many" annotations, where the tool is supposed to check our=
work. Safe code has few annotations; trusted code has more annotations.</d=
iv><div>- Code with no annotations, where we admit that we are doing unsafe=
things (and suppressing the tool) but promise that it's okay.</div><di=
v>(And of course there might be some code with "insufficiently many&qu=
ot; annotations, which will be rejected by the tool.)</div><div><br></div><=
div>This sounds like it could all be done with something as simple as "=
;#pragma checking on" and "#pragma checking off" (say, at fu=
nction granularity).</div><div>I don't think it requires or even sugges=
ts any=C2=A0<i>core language</i> changes.</div><div><br></div><div>It seems=
to me that the hard work here (which, again, at least some of which is bei=
ng done by the Contracts people) is in designing the proof-checking tool an=
d in designing the annotation syntax that allows us to communicate our inva=
riants to the tool (e.g. the syntax of the operands to [[expects:]] and [[e=
nsures:]]).</div><div><br></div><div>=E2=80=93Arthur</div><div><br></div><d=
iv>P.S. =E2=80=94 If there is a flaw in my argument, I think it is that I a=
m combining both "undesired behavior" and "undefined behavio=
r" under the single rubric of "program incorrectness." I thi=
nk Rust's "safe" corresponds not to "provably correct&qu=
ot; but merely "provably <i>not undefined behavior</i>" (i.e. eac=
h function's precondition is merely "UB has not yet occurred"=
and its postcondition is "UB has still not occurred"). Unfortuna=
tely I can't see how to achieve "provably <i>not undefined behavio=
r</i>" in C++ given the existence of multithreading and non-owning ref=
erences.</div><blockquote class=3D"gmail_quote" style=3D"margin: 0;margin-l=
eft: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr"=
>
</div></blockquote></div>
<p></p>
-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals" group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/85942f26-7a66-4543-9a38-d46a1bdf6cb3%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/85942f26-7a66-4543-9a38-d46a1bdf6cb3=
%40isocpp.org</a>.<br />
------=_Part_923_870154088.1521146174698--
------=_Part_922_2039975677.1521146174697--
.
Author: Edward Catmur <ed@catmur.co.uk>
Date: Thu, 15 Mar 2018 16:46:15 -0700 (PDT)
Raw View
------=_Part_472_1564495604.1521157575355
Content-Type: multipart/alternative;
boundary="----=_Part_473_402210181.1521157575356"
------=_Part_473_402210181.1521157575356
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
On Thursday, 15 March 2018 20:36:14 UTC, Arthur O'Dwyer wrote:
>
> On Tuesday, March 13, 2018 at 4:32:51 PM UTC-7, Mikl=C3=B3s P=C3=A1l wrot=
e:
>>
>> Proposed qualifiers:=20
>>
>> =E2=80=9Csafe=E2=80=9D: qualifies functions, where unsafe coding techniq=
ues are not=20
>> allowed by the compiler.
>>
>> =E2=80=9Ctrusted=E2=80=9D: qualifies functions, where unsafe coding tech=
niques are=20
>> allowed, but their correctness is proven by the author.
>>
>> Unqualified code: functions, where unsafe coding techniques are allowed,=
=20
>> and their correctness is unknown.
>>
>
> This idea is very similar to Rust in theory. But in practice, in C++, I=
=20
> guess I don't see why you need these qualifiers at all.
>
> In the definition of "trusted"-qualified code, you say that the=20
> correctness of trusted code must be "proven". If this means an informal,=
=20
> math-style paper proof, then there is no difference in practice between=
=20
> "trusted" and "unqualified" code =E2=80=94 both of them are formally unpr=
oven and=20
> unsafe, with some human being standing outside the computer going "hey,=
=20
> trust me, I write good code."
> So let's assume that by "proven" you mean in the formal program-proof=20
> sense: "trusted" code may use unsafe constructs, but it carries a program=
=20
> proof of its correctness, using annotations essentially like the Contract=
s=20
> proposals coming from people like Lisa Lippincott. The compiler (or some=
=20
> compiler-like tool) can read these annotations and check them for=20
> correctness-of-proof.
>
> So then in the definition of "safe"-qualified code, you say that the=20
> compiler should disallow "unsafe" coding techniques. The only meaning I c=
an=20
> assign to the word "unsafe" here is "coding techniques that (might) lead =
to=20
> program-incorrectness." So, in "safe"-qualified code, the compiler will b=
e=20
> checking that the code is provably correct. In other words, there is no=
=20
> difference between "safe"-qualified code and "trusted"-qualified code,=20
> except that in "safe" code we expect to write fewer annotations. (But=20
> certainly we can't write *no* annotations =E2=80=94 since the compiler is=
to=20
> check the correctness of our code, we still need to tell the compiler wha=
t=20
> it *means* to be correct! That is, we must annotate our "safe"-qualified=
=20
> code with preconditions and postconditions anyway.)
>
> So at this point we have two kinds of code:
> - Code with "sufficiently many" annotations, where the tool is supposed t=
o=20
> check our work. Safe code has few annotations; trusted code has more=20
> annotations.
> - Code with no annotations, where we admit that we are doing unsafe thing=
s=20
> (and suppressing the tool) but promise that it's okay.
> (And of course there might be some code with "insufficiently many"=20
> annotations, which will be rejected by the tool.)
>
> This sounds like it could all be done with something as simple as "#pragm=
a=20
> checking on" and "#pragma checking off" (say, at function granularity).
> I don't think it requires or even suggests any *core language* changes.
>
> It seems to me that the hard work here (which, again, at least some of=20
> which is being done by the Contracts people) is in designing the=20
> proof-checking tool and in designing the annotation syntax that allows us=
=20
> to communicate our invariants to the tool (e.g. the syntax of the operand=
s=20
> to [[expects:]] and [[ensures:]]).
>
> =E2=80=93Arthur
>
> P.S. =E2=80=94 If there is a flaw in my argument, I think it is that I am=
=20
> combining both "undesired behavior" and "undefined behavior" under the=20
> single rubric of "program incorrectness." I think Rust's "safe" correspon=
ds=20
> not to "provably correct" but merely "provably *not undefined behavior*"=
=20
> (i.e. each function's precondition is merely "UB has not yet occurred" an=
d=20
> its postcondition is "UB has still not occurred"). Unfortunately I can't=
=20
> see how to achieve "provably *not undefined behavior*" in C++ given the=
=20
> existence of multithreading and non-owning references.
>
We already have "provably not undefined behavior"; it's spelled constexpr.=
=20
This is achieved by banning access to mutable state external to the=20
evaluation in question.=20
Unfortunately, just because a function is constexpr doesn't mean it's safe=
=20
to process untrusted user input; a constexpr function only has to be=20
UB-free on a non-empty subset of inputs. But perhaps this could be a=20
starting point.
--=20
You received this message because you are subscribed to the Google Groups "=
ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to std-proposals+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
To view this discussion on the web visit https://groups.google.com/a/isocpp=
..org/d/msgid/std-proposals/9ac56f78-bd1c-48b9-a142-215d1028a826%40isocpp.or=
g.
------=_Part_473_402210181.1521157575356
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr"><br><br>On Thursday, 15 March 2018 20:36:14 UTC, Arthur O&=
#39;Dwyer wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0;margi=
n-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"l=
tr">On Tuesday, March 13, 2018 at 4:32:51 PM UTC-7, Mikl=C3=B3s P=C3=A1l wr=
ote:<blockquote class=3D"gmail_quote" style=3D"margin:0;margin-left:0.8ex;b=
order-left:1px #ccc solid;padding-left:1ex"><div dir=3D"ltr">
<h1><span style=3D"font-size:13px">Proposed
qualifiers:</span></h1>
<p class=3D"MsoNormal"><span lang=3D"EN-US">=E2=80=9Csafe=E2=80=9D:
qualifies functions, where unsafe coding techniques are not allowed by the
compiler.</span></p>
<p class=3D"MsoNormal"><span lang=3D"EN-US">=E2=80=9Ctrusted=E2=80=9D:
qualifies functions, where unsafe coding techniques are allowed, but their
correctness is proven by the author.</span></p>
<p class=3D"MsoNormal"><span lang=3D"EN-US">Unqualified
code: functions, where unsafe coding techniques are allowed, and their
correctness is unknown.</span></p></div></blockquote><div><br></div><div>Th=
is idea is very similar to Rust in theory. But in practice, in C++, I guess=
I don't see why you need these qualifiers at all.</div><div><br></div>=
<div>In the definition of "trusted"-qualified code, you say that =
the correctness of trusted code must be "proven". If this means a=
n informal, math-style paper proof, then there is no difference in practice=
between "trusted" and "unqualified" code =E2=80=94 bot=
h of them are formally unproven and unsafe, with some human being standing =
outside the computer going "hey, trust me, I write good code."</d=
iv><div>So let's assume that by "proven" you mean in the form=
al program-proof sense: "trusted" code may use unsafe constructs,=
but it carries a program proof of its correctness, using annotations essen=
tially like the Contracts proposals coming from people like Lisa Lippincott=
.. The compiler (or some compiler-like tool) can read these annotations and =
check them for correctness-of-proof.</div><div><br></div><div>So then in th=
e definition of "safe"-qualified code, you say that the compiler =
should disallow "unsafe" coding techniques. The only meaning I ca=
n assign to the word "unsafe" here is "coding techniques tha=
t (might) lead to program-incorrectness." So, in "safe"-qual=
ified code, the compiler will be checking that the code is provably correct=
.. In other words, there is no difference between "safe"-qualified=
code and "trusted"-qualified code, except that in "safe&quo=
t; code we expect to write fewer annotations. (But certainly we can't w=
rite <i>no</i> annotations =E2=80=94 since the compiler is to check the cor=
rectness of our code, we still need to tell the compiler what it <i>means</=
i> to be correct! That is, we must annotate our "safe"-qualified =
code with preconditions and postconditions anyway.)</div><div><br></div><di=
v>So at this point we have two kinds of code:</div><div>- Code with "s=
ufficiently many" annotations, where the tool is supposed to check our=
work. Safe code has few annotations; trusted code has more annotations.</d=
iv><div>- Code with no annotations, where we admit that we are doing unsafe=
things (and suppressing the tool) but promise that it's okay.</div><di=
v>(And of course there might be some code with "insufficiently many&qu=
ot; annotations, which will be rejected by the tool.)</div><div><br></div><=
div>This sounds like it could all be done with something as simple as "=
;#pragma checking on" and "#pragma checking off" (say, at fu=
nction granularity).</div><div>I don't think it requires or even sugges=
ts any=C2=A0<i>core language</i> changes.</div><div><br></div><div>It seems=
to me that the hard work here (which, again, at least some of which is bei=
ng done by the Contracts people) is in designing the proof-checking tool an=
d in designing the annotation syntax that allows us to communicate our inva=
riants to the tool (e.g. the syntax of the operands to [[expects:]] and [[e=
nsures:]]).</div><div><br></div><div>=E2=80=93Arthur</div><div><br></div><d=
iv>P.S. =E2=80=94 If there is a flaw in my argument, I think it is that I a=
m combining both "undesired behavior" and "undefined behavio=
r" under the single rubric of "program incorrectness." I thi=
nk Rust's "safe" corresponds not to "provably correct&qu=
ot; but merely "provably <i>not undefined behavior</i>" (i.e. eac=
h function's precondition is merely "UB has not yet occurred"=
and its postcondition is "UB has still not occurred"). Unfortuna=
tely I can't see how to achieve "provably <i>not undefined behavio=
r</i>" in C++ given the existence of multithreading and non-owning ref=
erences.</div></div></blockquote><div><br></div><div>We already have "=
provably not undefined behavior"; it's spelled constexpr. This is =
achieved by banning access to mutable state external to the evaluation in q=
uestion.=C2=A0</div><div><br></div><div>Unfortunately, just because a funct=
ion is constexpr doesn't mean it's safe to process untrusted user i=
nput; a constexpr function only has to be UB-free on a non-empty subset of =
inputs. But perhaps this could be a starting point.</div></div>
<p></p>
-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals" group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/9ac56f78-bd1c-48b9-a142-215d1028a826%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/9ac56f78-bd1c-48b9-a142-215d1028a826=
%40isocpp.org</a>.<br />
------=_Part_473_402210181.1521157575356--
------=_Part_472_1564495604.1521157575355--
.
Author: emuzychenko@gmail.com
Date: Mon, 19 Mar 2018 01:44:08 -0700 (PDT)
Raw View
------=_Part_10538_302978448.1521449048640
Content-Type: multipart/alternative;
boundary="----=_Part_10539_93208742.1521449048640"
------=_Part_10539_93208742.1521449048640
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
On Wednesday, March 14, 2018 at 6:32:51 AM UTC+7, Mikl=C3=B3s P=C3=A1l wrot=
e:
>
> This is more an attempt to take the benefit of both safety enforcements=
=20
> and unrestricted coding.
>
It might be implemented in terms of more common and universal custom=20
attributes idea=20
<https://groups.google.com/a/isocpp.org/forum/#!topic/std-proposals/Mt9BDii=
sEDs>=20
I published recently.
>
--=20
You received this message because you are subscribed to the Google Groups "=
ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to std-proposals+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
To view this discussion on the web visit https://groups.google.com/a/isocpp=
..org/d/msgid/std-proposals/bca14045-9a28-4694-8cd6-fafbf6069913%40isocpp.or=
g.
------=_Part_10539_93208742.1521449048640
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr">On Wednesday, March 14, 2018 at 6:32:51 AM UTC+7, Mikl=C3=
=B3s P=C3=A1l wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0;ma=
rgin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=
=3D"ltr"><p>This is more an attempt to take the benefit of both safety enfo=
rcements and unrestricted coding.</p></div></blockquote><div dir=3D"ltr"><p=
><br></p><p>It might be implemented in terms of more common and universal <=
a href=3D"https://groups.google.com/a/isocpp.org/forum/#!topic/std-proposal=
s/Mt9BDiisEDs">custom attributes idea</a> I published recently.<br></p></di=
v><blockquote class=3D"gmail_quote" style=3D"margin: 0;margin-left: 0.8ex;b=
order-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr"></div></blo=
ckquote></div>
<p></p>
-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals" group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/bca14045-9a28-4694-8cd6-fafbf6069913%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/bca14045-9a28-4694-8cd6-fafbf6069913=
%40isocpp.org</a>.<br />
------=_Part_10539_93208742.1521449048640--
------=_Part_10538_302978448.1521449048640--
.