Topic: Re: [std-proposals] Re: Enforcing safe coding techni
Author: Jonathan Coe <jonathanbcoe@gmail.com>
Date: Wed, 14 Mar 2018 00:04:50 -0400
Raw View
--Apple-Mail-BDFF506A-E25C-49B4-A85D-5BEF185A0D5B
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
It might be interesting to add a series of clang tidy checks for unsafe cod=
e which could be selectively enabled. That might give implementation experi=
ence as to what can be checked for.
> On 13 Mar 2018, at 22:51, Nicol Bolas <jmckesson@gmail.com> wrote:
>=20
> Consider this:
>=20
> struct S
> {
> shared_ptr<S> ptr;
> int val;
> };
>=20
> auto ptr1 =3D make_shared<S>(nullptr, 4);
> auto ptr2 =3D make_shared<S>(ptr1, 6);
> auto ptr3 =3D make_shared<S>(ptr2, -3);
> ptr1.ptr =3D ptr3;
>=20
> 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?
>=20
> 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 hav=
ing language features that give them a false sense of security about how "s=
afe" their code is.
>=20
> Now consider this:
>=20
> int arr[3] =3D {5, 2, -13};
> arr[1] =3D 6;
>=20
> 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?
>=20
> 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 "safer", but that's a lot different from "safe".
>=20
> And that sort of thing is far better left up to each individual programme=
r and their static analysis tools of choice.
> --=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=
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/isoc=
pp.org/d/msgid/std-proposals/1a250082-a1d8-4f36-93a3-8540056ff279%40isocpp.=
org.
--=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/4BDA3D07-62AA-4B30-BCA0-875A446F6B23%40gmail.com=
..
--Apple-Mail-BDFF506A-E25C-49B4-A85D-5BEF185A0D5B
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<html><head><meta http-equiv=3D"content-type" content=3D"text/html; charset=
=3Dutf-8"></head><body dir=3D"auto"><div></div><div>It might be interesting=
to add a series of clang tidy checks for unsafe code which could be select=
ively enabled. That might give implementation experience as to what can be =
checked for.</div><div><br>On 13 Mar 2018, at 22:51, Nicol Bolas <<a hre=
f=3D"mailto:jmckesson@gmail.com">jmckesson@gmail.com</a>> wrote:<br><br>=
</div><blockquote type=3D"cite"><div><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; border-width: 1px; overflow-wrap: break-wo=
rd;" class=3D"prettyprint"><code class=3D"prettyprint"><div class=3D"subpre=
ttyprint"><span style=3D"color: #008;" class=3D"styled-by-prettify">struct<=
/span><span style=3D"color: #000;" class=3D"styled-by-prettify"> S<br></spa=
n><span style=3D"color: #660;" class=3D"styled-by-prettify">{</span><span s=
tyle=3D"color: #000;" class=3D"styled-by-prettify"><br> shared_ptr</s=
pan><span style=3D"color: #660;" class=3D"styled-by-prettify"><</span><s=
pan 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"co=
lor: #000;" class=3D"styled-by-prettify"> ptr</span><span style=3D"color: #=
660;" class=3D"styled-by-prettify">;</span><span style=3D"color: #000;" cla=
ss=3D"styled-by-prettify"><br> </span><span style=3D"color: #008;" cl=
ass=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-prett=
ify"><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;" class=3D"styled-by-prettify">auto</span>=
<span style=3D"color: #000;" class=3D"styled-by-prettify"> ptr1 </span><spa=
n 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 sty=
le=3D"color: #660;" class=3D"styled-by-prettify"><</span><span style=3D"=
color: #000;" class=3D"styled-by-prettify">S</span><span style=3D"color: #6=
60;" class=3D"styled-by-prettify">>(</span><span style=3D"color: #008;" =
class=3D"styled-by-prettify">nullptr</span><span style=3D"color: #660;" cla=
ss=3D"styled-by-prettify">,</span><span style=3D"color: #000;" class=3D"sty=
led-by-prettify"> </span><span style=3D"color: #066;" class=3D"styled-by-pr=
ettify">4</span><span style=3D"color: #660;" class=3D"styled-by-prettify">)=
;</span><span style=3D"color: #000;" class=3D"styled-by-prettify"><br></spa=
n><span style=3D"color: #008;" class=3D"styled-by-prettify">auto</span><spa=
n style=3D"color: #000;" class=3D"styled-by-prettify"> ptr2 </span><span st=
yle=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"styled-by-prettify"><</span><span style=3D"co=
lor: #000;" class=3D"styled-by-prettify">S</span><span style=3D"color: #660=
;" class=3D"styled-by-prettify">>(</span><span style=3D"color: #000;" cl=
ass=3D"styled-by-prettify">ptr1</span><span style=3D"color: #660;" class=3D=
"styled-by-prettify">,</span><span style=3D"color: #000;" class=3D"styled-b=
y-prettify"> </span><span style=3D"color: #066;" class=3D"styled-by-prettif=
y">6</span><span style=3D"color: #660;" class=3D"styled-by-prettify">);</sp=
an><span style=3D"color: #000;" class=3D"styled-by-prettify"><br></span><sp=
an style=3D"color: #008;" class=3D"styled-by-prettify">auto</span><span sty=
le=3D"color: #000;" class=3D"styled-by-prettify"> ptr3 </span><span style=
=3D"color: #660;" class=3D"styled-by-prettify">=3D</span><span style=3D"col=
or: #000;" class=3D"styled-by-prettify"> make_shared</span><span style=3D"c=
olor: #660;" class=3D"styled-by-prettify"><</span><span style=3D"color: =
#000;" class=3D"styled-by-prettify">S</span><span style=3D"color: #660;" cl=
ass=3D"styled-by-prettify">>(</span><span style=3D"color: #000;" class=
=3D"styled-by-prettify">ptr2</span><span style=3D"color: #660;" class=3D"st=
yled-by-prettify">,</span><span style=3D"color: #000;" class=3D"styled-by-p=
rettify"> </span><span style=3D"color: #660;" class=3D"styled-by-prettify">=
-</span><span style=3D"color: #066;" class=3D"styled-by-prettify">3</span><=
span style=3D"color: #660;" class=3D"styled-by-prettify">);</span><span sty=
le=3D"color: #000;" class=3D"styled-by-prettify"><br>ptr1</span><span style=
=3D"color: #660;" class=3D"styled-by-prettify">.</span><span style=3D"color=
: #000;" class=3D"styled-by-prettify">ptr </span><span style=3D"color: #660=
;" class=3D"styled-by-prettify">=3D</span><span style=3D"color: #000;" clas=
s=3D"styled-by-prettify"> ptr3</span><span style=3D"color: #660;" class=3D"=
styled-by-prettify">;</span><span style=3D"color: #000;" class=3D"styled-by=
-prettify"><br></span></div></code></div><br>Ignore the fact that `make_sha=
red` doesn't work with aggregates. Can you provide a simple rule which woul=
d let the compiler decide that this code is "unsafe"? What if each of those=
pointer creation and assignment functions were hidden behind several layer=
s of functions, so that the compiler can't see everything?<br><br>Just beca=
use 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 bet=
ter <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 is.<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"prettypr=
int"><div class=3D"subprettyprint"><span style=3D"color: #008;" class=3D"st=
yled-by-prettify">int</span><span style=3D"color: #000;" class=3D"styled-by=
-prettify"> arr</span><span style=3D"color: #660;" class=3D"styled-by-prett=
ify">[</span><span style=3D"color: #066;" class=3D"styled-by-prettify">3</s=
pan><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 style=3D"color:=
#000;" class=3D"styled-by-prettify"> </span><span style=3D"color: #660;" c=
lass=3D"styled-by-prettify">{</span><span style=3D"color: #066;" class=3D"s=
tyled-by-prettify">5</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: #066;" class=3D"styled-by-prettify">2</span>=
<span style=3D"color: #660;" class=3D"styled-by-prettify">,</span><span sty=
le=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=3D"col=
or: #660;" class=3D"styled-by-prettify">-</span><span style=3D"color: #066;=
" class=3D"styled-by-prettify">13</span><span style=3D"color: #660;" class=
=3D"styled-by-prettify">};</span><span style=3D"color: #000;" class=3D"styl=
ed-by-prettify"><br>arr</span><span style=3D"color: #660;" class=3D"styled-=
by-prettify">[</span><span style=3D"color: #066;" class=3D"styled-by-pretti=
fy">1</span><span style=3D"color: #660;" class=3D"styled-by-prettify">]</sp=
an><span style=3D"color: #000;" class=3D"styled-by-prettify"> </span><span =
style=3D"color: #660;" class=3D"styled-by-prettify">=3D</span><span style=
=3D"color: #000;" class=3D"styled-by-prettify"> </span><span style=3D"color=
: #066;" class=3D"styled-by-prettify">6</span><span style=3D"color: #660;" =
class=3D"styled-by-prettify">;</span><span style=3D"color: #000;" class=3D"=
styled-by-prettify"><br></span></div></code></div><br>This is perfectly, 10=
0% 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 "unsa=
fe", what you really mean is "low-level" or "not-modern". Neither is genuin=
ely "safe"; it may be "safe<u><i><b>r</b></i></u>", but that's a lot differ=
ent from "safe".<br><br>And that sort of thing is far better left up to eac=
h individual programmer and their static analysis tools of choice.<br></div=
>
<p></p>
-- <br>
You received this message because you are subscribed to the Google Groups "=
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.goo=
gle.com/a/isocpp.org/d/msgid/std-proposals/1a250082-a1d8-4f36-93a3-8540056f=
f279%40isocpp.org</a>.<br>
</div></blockquote></body></html>
<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/4BDA3D07-62AA-4B30-BCA0-875A446F6B23%=
40gmail.com?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/4BDA3D07-62AA-4B30-BCA0-875A446F6B23%=
40gmail.com</a>.<br />
--Apple-Mail-BDFF506A-E25C-49B4-A85D-5BEF185A0D5B--
.
Author: =?UTF-8?B?TWlrbMOzcyBQw6Fs?= <palmiklos@gmail.com>
Date: Sun, 18 Mar 2018 22:39:41 +0100
Raw View
--000000000000d91cfb0567b6ad00
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
Dear All,
I accept your opoinions, and accept that following my proposal, we can't
reach proven code safty.
My goal was to make the development of large apps safer by disallowing
coding techniquies, which frequently lead to errors, and have safe
replacements, but not restrincting the language for the development of the
whole source code.
Code annotations (pre and post-contions, etc.) with source code analysers
probably can provide better safety.
***** Fingers crossed for C++ contracts. *****
Anyway, I clarify some points:
>> ...then there is no difference in practice between "trusted" and
"unqualified" code
True, if we consider the code itself, but my rules allow "trusted" code,
but don't allow unqualified code to be called from qualified code. This is
the difference.
Unqualified code is defined for compatibility.
>> ...in "safe"-qualified code, the compiler will be checking that the code
is provably correct.
No. In my point of view, the compiler doesn't prove correctness of "safe"
code, just disallows some unsafe language constructions.
>> We already have "provably not undefined behavior"; it's spelled
constexpr.
I agree, and like this recognition, but my proposal is more about run-time
behavior of non-constexpr code.
>> That is, we must annotate our "safe"-qualified code with preconditions
and postconditions anyway.)
In my proposal, I didn't consider code annotations designed for giving
additional information for code correctness analyser tools (contracts). I
started out from the current C++ language. Such annotations can make unsafe
constructions safe again. For example, let's start with the unsafe strlen.
If a pre-condition requires that the input is a null-terminated string
having a given maximum length, and a code analyser tool can prove that the
pre-condition is met on each usage, our call of strlen is safe.
I've already used Microsof's SAL annotations and static code analyser, and
found it useful for making better, safer code. I'd be glad if such
annotations (contracts) appeared in a future C++ standard.
On Fri, Mar 16, 2018 at 12:46 AM, Edward Catmur <ed@catmur.co.uk> wrote:
>
>
> 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 wro=
te:
>>>
>>> Proposed qualifiers:
>>>
>>> =E2=80=9Csafe=E2=80=9D: qualifies functions, where unsafe coding techni=
ques are not
>>> allowed by the compiler.
>>>
>>> =E2=80=9Ctrusted=E2=80=9D: qualifies functions, where unsafe coding tec=
hniques are
>>> allowed, but their correctness is proven by the author.
>>>
>>> Unqualified code: functions, where unsafe coding techniques are allowed=
,
>>> and their correctness is unknown.
>>>
>>
>> This 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.
>>
>> In the definition of "trusted"-qualified code, you say that the
>> correctness of trusted code must be "proven". If this means an informal,
>> math-style paper proof, then there is no difference in practice between
>> "trusted" and "unqualified" code =E2=80=94 both of them are formally unp=
roven and
>> unsafe, with some human being standing outside the computer going "hey,
>> trust me, I write good code."
>> So let's assume that by "proven" you mean in the formal program-proof
>> sense: "trusted" code may use unsafe constructs, but it carries a progra=
m
>> proof of its correctness, using annotations essentially like the Contrac=
ts
>> 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.
>>
>> So then in the definition of "safe"-qualified code, you say that the
>> compiler should disallow "unsafe" coding techniques. The only meaning I =
can
>> assign to the word "unsafe" here is "coding techniques that (might) lead=
to
>> program-incorrectness." So, in "safe"-qualified 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" code we expect to write fewer annotations. (But
>> certainly we can't write *no* annotations =E2=80=94 since the compiler i=
s to
>> check the correctness of our code, we still need to tell the compiler wh=
at
>> it *means* to be correct! That is, we must annotate our "safe"-qualified
>> 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
>> to check our work. Safe code has few annotations; trusted code has more
>> annotations.
>> - Code with no annotations, where we admit that we are doing unsafe
>> things (and suppressing the tool) but promise that it's okay.
>> (And of course there might be some code with "insufficiently many"
>> annotations, which will be rejected by the tool.)
>>
>> This sounds like it could all be done with something as simple as
>> "#pragma 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
>> which is being done by the Contracts people) is in designing the
>> proof-checking tool and in designing the annotation syntax that allows u=
s
>> to communicate our invariants to the tool (e.g. the syntax of the operan=
ds
>> 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 a=
m
>> combining both "undesired behavior" and "undefined behavior" under the
>> single rubric of "program incorrectness." I think Rust's "safe" correspo=
nds
>> not to "provably correct" but merely "provably *not undefined behavior*"
>> (i.e. each function's precondition is merely "UB has not yet occurred" a=
nd
>> its postcondition is "UB has still not occurred"). Unfortunately I can't
>> see how to achieve "provably *not undefined behavior*" in C++ given the
>> existence of multithreading and non-owning references.
>>
>
> 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 question.
>
> Unfortunately, just because a function is constexpr doesn't mean it's saf=
e
> to process untrusted user input; a constexpr function only has to be
> UB-free on a non-empty subset of inputs. But perhaps this could be a
> starting point.
>
> --
> You received this message because you are subscribed to a topic in the
> Google Groups "ISO C++ Standard - Future Proposals" group.
> To unsubscribe from this topic, visit https://groups.google.com/a/
> isocpp.org/d/topic/std-proposals/DyAMYDvMPg8/unsubscribe.
> To unsubscribe from this group and all its topics, 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/9ac56f78-bd1c-48b9-
> a142-215d1028a826%40isocpp.org
> <https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/9ac56f78-bd=
1c-48b9-a142-215d1028a826%40isocpp.org?utm_medium=3Demail&utm_source=3Dfoot=
er>
> .
>
--=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/CAHP9XZGA7gh9P6DBykOxKTKTZWNgyBk_rF3y1EgyFKMkXkN=
i1Q%40mail.gmail.com.
--000000000000d91cfb0567b6ad00
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
<div dir=3D"ltr"><div><div><div><div><div>Dear All,<br><br></div><div>I acc=
ept your opoinions, and accept that following my proposal, we can't rea=
ch proven code safty.<br><br>My goal was to make the development of large a=
pps safer by disallowing coding techniquies, which frequently lead to error=
s, and have safe replacements, but not restrincting the language for the de=
velopment of the whole source code.<br><br>Code annotations (pre and post-c=
ontions, etc.) with source code analysers probably can provide better safet=
y.<br><br>***** Fingers crossed for C++ contracts. *****<br><br>Anyway, I c=
larify some points:<br></div><div><br>>> ...then there is no differen=
ce in practice between "trusted" and "unqualified" code=
<br></div><br></div>True, if we consider the code itself, but my rules allo=
w "trusted" code, but don't allow unqualified code to be call=
ed from qualified code. This is the difference.<br></div><div>Unqualified c=
ode is defined for compatibility.<br></div><div><br>>>
<span class=3D"gmail-im">...in "safe"-qualified code, the compile=
r will be checking that the code is provably correct.</span><br><br></div>N=
o. In my point of view, the compiler doesn't prove correctness of "=
;safe" code, just disallows some unsafe language constructions.<br><br=
>>>=20
We already have "provably not undefined behavior"; it's spell=
ed constexpr.<br><br></div><div>I agree, and like this recognition, but my =
proposal is more about run-time behavior of non-constexpr code.<br><br>>=
>=20
<span class=3D"gmail-im">That is, we must annotate our "safe"-qua=
lified code with preconditions and postconditions anyway.)</span>
<br></div><br>In my proposal, I didn't consider code annotations design=
ed for giving additional information for code correctness analyser tools (c=
ontracts). I started out from the current C++ language. Such annotations ca=
n make unsafe constructions safe again. For example, let's start with t=
he unsafe strlen. If a pre-condition requires that the input is a null-term=
inated string having a given maximum length, and a code analyser tool can p=
rove that the pre-condition is met on each usage, our call of strlen is saf=
e.<br><br>I've already used Microsof's SAL annotations and static c=
ode analyser, and found it useful for making better, safer code. I'd be=
glad if such annotations (contracts) appeared in a future C++ standard.<br=
><br><div><br></div></div></div><div class=3D"gmail_extra"><br><div class=
=3D"gmail_quote">On Fri, Mar 16, 2018 at 12:46 AM, Edward Catmur <span dir=
=3D"ltr"><<a href=3D"mailto:ed@catmur.co.uk" target=3D"_blank">ed@catmur=
..co.uk</a>></span> wrote:<br><blockquote class=3D"gmail_quote" style=3D"=
margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir=3D"=
ltr"><span class=3D""><br><br>On Thursday, 15 March 2018 20:36:14 UTC, Arth=
ur O'Dwyer wrote:<blockquote class=3D"gmail_quote" style=3D"margin:0;m=
argin-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></span><div>We already have=
"provably not undefined behavior"; it's spelled constexpr. T=
his is achieved by banning access to mutable state external to the evaluati=
on in question.=C2=A0</div><div><br></div><div>Unfortunately, just because =
a function is constexpr doesn't mean it's safe to process untrusted=
user input; a constexpr function only has to be UB-free on a non-empty sub=
set of inputs. But perhaps this could be a starting point.</div></div><span=
class=3D"">
<p></p>
-- <br>
You received this message because you are subscribed to a topic in the Goog=
le Groups "ISO C++ Standard - Future Proposals" group.<br>
To unsubscribe from this topic, visit <a href=3D"https://groups.google.com/=
a/isocpp.org/d/topic/std-proposals/DyAMYDvMPg8/unsubscribe" target=3D"_blan=
k">https://groups.google.com/a/<wbr>isocpp.org/d/topic/std-<wbr>proposals/D=
yAMYDvMPg8/<wbr>unsubscribe</a>.<br>
To unsubscribe from this group and all its topics, send an email to <a href=
=3D"mailto:std-proposals+unsubscribe@isocpp.org" target=3D"_blank">std-prop=
osals+unsubscribe@<wbr>isocpp.org</a>.<br>
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org" target=3D"_blank">std-proposals@isocpp.org</a>.<br></span>
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" target=3D"_blank">=
https://groups.google.com/a/<wbr>isocpp.org/d/msgid/std-<wbr>proposals/9ac5=
6f78-bd1c-48b9-<wbr>a142-215d1028a826%40isocpp.org</a><wbr>.<br>
</blockquote></div><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/CAHP9XZGA7gh9P6DBykOxKTKTZWNgyBk_rF3y=
1EgyFKMkXkNi1Q%40mail.gmail.com?utm_medium=3Demail&utm_source=3Dfooter">htt=
ps://groups.google.com/a/isocpp.org/d/msgid/std-proposals/CAHP9XZGA7gh9P6DB=
ykOxKTKTZWNgyBk_rF3y1EgyFKMkXkNi1Q%40mail.gmail.com</a>.<br />
--000000000000d91cfb0567b6ad00--
.