Ironclad C++

2013-08-03 Thread bearophile
"Ironclad C++, A Library-Augmented Type-Safe Subset of C++" by Christian DeLozier et al: http://repository.upenn.edu/cis_reports/982/ It's a strict subset of C++ plus added some libraries and some static verifiers. The purpose is to have a safer C++. It has some similarities

Re: Ironclad C++

2013-08-03 Thread Walter Bright
On 8/3/2013 4:32 PM, bearophile wrote: The paper explains the various cases: assign from ptr into lptr, assign from lptr into ptr, and assign from lptr into lptr. So with a mix of run-time tests and a small amount of static analysis the code is safe and fast enough. It seems a simple enough idea

Re: Ironclad C++

2013-08-03 Thread Timon Gehr
On 08/04/2013 01:55 AM, Walter Bright wrote: On 8/3/2013 4:32 PM, bearophile wrote: The paper explains the various cases: assign from ptr into lptr, assign from lptr into ptr, and assign from lptr into lptr. So with a mix of run-time tests and a small amount of static analysis the code is safe

Re: Ironclad C++

2013-08-03 Thread Walter Bright
On 8/3/2013 5:49 PM, Timon Gehr wrote: On 08/04/2013 01:55 AM, Walter Bright wrote: On 8/3/2013 4:32 PM, bearophile wrote: The paper explains the various cases: assign from ptr into lptr, assign from lptr into ptr, and assign from lptr into lptr. So with a mix of run-time tests and a small amo

Re: Ironclad C++

2013-08-03 Thread Timon Gehr
On 08/04/2013 04:06 AM, Walter Bright wrote: On 8/3/2013 5:49 PM, Timon Gehr wrote: On 08/04/2013 01:55 AM, Walter Bright wrote: On 8/3/2013 4:32 PM, bearophile wrote: The paper explains the various cases: assign from ptr into lptr, assign from lptr into ptr, and assign from lptr into lptr. S

Re: Ironclad C++

2013-08-03 Thread Walter Bright
On 8/3/2013 7:08 PM, Timon Gehr wrote: On 08/04/2013 04:06 AM, Walter Bright wrote: On 8/3/2013 5:49 PM, Timon Gehr wrote: On 08/04/2013 01:55 AM, Walter Bright wrote: On 8/3/2013 4:32 PM, bearophile wrote: The paper explains the various cases: assign from ptr into lptr, assign from lptr into

Re: Ironclad C++

2013-08-03 Thread Timon Gehr
On 08/04/2013 04:28 AM, Walter Bright wrote: On 8/3/2013 7:08 PM, Timon Gehr wrote: On 08/04/2013 04:06 AM, Walter Bright wrote: On 8/3/2013 5:49 PM, Timon Gehr wrote: On 08/04/2013 01:55 AM, Walter Bright wrote: On 8/3/2013 4:32 PM, bearophile wrote: The paper explains the various cases: as

Re: Ironclad C++

2013-08-03 Thread Walter Bright
On 8/3/2013 7:41 PM, Timon Gehr wrote: Yes, but as far as I understood it you can assign lptr back to ptr implicitly by paying for a runtime check. It's what D will be doing with T* <-> ref T, right? I thought the idea was to use the type system to avoid runtime checks. (The general problem

Re: Ironclad C++

2013-08-04 Thread Kagamin
On Sunday, 4 August 2013 at 02:41:18 UTC, Timon Gehr wrote: D's inout is a somewhat failed attempt Why?

Re: Ironclad C++

2013-08-04 Thread Araq
Consider the canonical example: void* foo(void *p) { return p; } Do you write an overload for each kind of pointer? Doesn't D already have that problem with its immutable/const pointers?

Re: Ironclad C++

2013-08-04 Thread deadalnix
On Sunday, 4 August 2013 at 09:52:01 UTC, Kagamin wrote: On Sunday, 4 August 2013 at 02:41:18 UTC, Timon Gehr wrote: D's inout is a somewhat failed attempt Why? It only work for qualifiers. The same issue arise in much for various form where inout can't do anything. What a bout a function

Re: Ironclad C++

2013-08-04 Thread Timon Gehr
On 08/04/2013 11:51 AM, Kagamin wrote: On Sunday, 4 August 2013 at 02:41:18 UTC, Timon Gehr wrote: D's inout is a somewhat failed attempt Why? Off the top of my head: - No naming or scoping: // is this ok? inout(int)* foo(inout(int)* a, inout(int)* delegate(inout(int)*) dg){ return dg(

Re: Ironclad C++

2013-08-04 Thread bearophile
Timon Gehr: Off the top of my head: Thank you. Is it right to add 'inout' the list of D2 features that will be deprecated and later removed? There are "simple" features, like a support for structurally typed tuples, that maybe can be designed well enough with the traditional method. But

Re: Ironclad C++

2013-08-04 Thread Walter Bright
On 8/4/2013 3:48 AM, Araq wrote: Consider the canonical example: void* foo(void *p) { return p; } Do you write an overload for each kind of pointer? Doesn't D already have that problem with its immutable/const pointers? Yes, and we've gone to considerable effort to deal with it, and th

Re: Ironclad C++

2013-08-04 Thread Walter Bright
On 8/4/2013 7:04 AM, deadalnix wrote: What a bout a function which is pure depending on if a function passed as parameter is pure or not ? or return a function the same way ? This is where attribute inference comes into play.

Re: Ironclad C++

2013-08-04 Thread Timon Gehr
On 08/04/2013 08:35 PM, Walter Bright wrote: On 8/4/2013 7:04 AM, deadalnix wrote: What a bout a function which is pure depending on if a function passed as parameter is pure or not ? or return a function the same way ? This is where attribute inference comes into play. (He is talking about

Re: Ironclad C++

2013-08-04 Thread Timon Gehr
On 08/04/2013 06:18 PM, bearophile wrote: Timon Gehr: Off the top of my head: Thank you. Is it right to add 'inout' the list of D2 features that will be deprecated and later removed? ... Maybe, but this is not my decision, and if it is removed it should be replaced. There are "simple"

Re: Ironclad C++

2013-08-04 Thread bearophile
Timon Gehr: Formal proofs require a formalization of language semantics. It's not just a matter of finding someone to carry out the proof. (Anyone can learn online how to do this.) I think you have too much faith in people intelligence (or just in my intelligence) :-) Bye, bearophile

Re: Ironclad C++

2013-08-04 Thread Timon Gehr
On 08/04/2013 11:55 PM, bearophile wrote: Timon Gehr: Formal proofs require a formalization of language semantics. It's not just a matter of finding someone to carry out the proof. (Anyone can learn online how to do this.) I think you have too much faith in people intelligence (or just in my

Re: Ironclad C++

2013-08-04 Thread Walter Bright
On 8/4/2013 8:04 AM, Timon Gehr wrote: Off the top of my head: If these are not in bugzilla, please add them.

Re: Ironclad C++

2013-08-04 Thread Timon Gehr
On 08/05/2013 12:35 AM, Walter Bright wrote: On 8/4/2013 8:04 AM, Timon Gehr wrote: Off the top of my head: If these are not in bugzilla, please add them. I have reported the unsoundness: http://d.puremagic.com/issues/show_bug.cgi?id=10758

Re: Ironclad C++

2013-08-04 Thread Walter Bright
On 8/4/2013 4:03 PM, Timon Gehr wrote: On 08/05/2013 12:35 AM, Walter Bright wrote: On 8/4/2013 8:04 AM, Timon Gehr wrote: Off the top of my head: If these are not in bugzilla, please add them. I have reported the unsoundness: http://d.puremagic.com/issues/show_bug.cgi?id=10758 Please

Re: Ironclad C++

2013-08-04 Thread Andre Artus
On Sunday, 4 August 2013 at 22:26:19 UTC, Timon Gehr wrote: On 08/04/2013 11:55 PM, bearophile wrote: Timon Gehr: Formal proofs require a formalization of language semantics. It's not just a matter of finding someone to carry out the proof. (Anyone can learn online how to do this.) I think

Re: Ironclad C++

2013-08-05 Thread Kagamin
On Sunday, 4 August 2013 at 15:04:48 UTC, Timon Gehr wrote: - No naming or scoping: OK, but I'm not sure naming and scoping buys you anything except for being more explicit, but explicity vs implicity is a tradeoff. I kinda understand the argument about dependent purity, but the problem with

Re: Ironclad C++

2013-08-05 Thread Kagamin
On Sunday, 4 August 2013 at 16:18:48 UTC, bearophile wrote: I am starting to think that to design type system features sometimes you need formal mathematics, otherwise you build a Swiss cheese. How would you account for yet undefined features like ARC?

Re: Ironclad C++

2013-08-05 Thread Timon Gehr
On 08/05/2013 10:44 PM, Kagamin wrote: On Sunday, 4 August 2013 at 15:04:48 UTC, Timon Gehr wrote: - No naming or scoping: OK, but I'm not sure naming and scoping buys you anything except for being more explicit, but explicity vs implicity is a tradeoff. I thought I had demonstrated that it

Re: Ironclad C++

2013-08-05 Thread deadalnix
On Sunday, 4 August 2013 at 15:04:48 UTC, Timon Gehr wrote: On 08/04/2013 11:51 AM, Kagamin wrote: On Sunday, 4 August 2013 at 02:41:18 UTC, Timon Gehr wrote: D's inout is a somewhat failed attempt Why? Off the top of my head: - No naming or scoping: // is this ok? inout(int)* foo(inout(i

Re: Ironclad C++

2013-08-06 Thread Kagamin
On Tuesday, 6 August 2013 at 02:11:54 UTC, Timon Gehr wrote: I thought I had demonstrated that it buys you more. It resolves the problem that scoping is ambiguous and that there can be only one 'inout' substitution per function application. It may look ambiguous to someone who doesn't know, ho

Re: Ironclad C++

2013-08-06 Thread Kagamin
On Tuesday, 6 August 2013 at 03:42:00 UTC, deadalnix wrote: The ambiguity lies in the fact that inout in the delegate may stand for foo's inout or delegate's inout. inout applies to parameters and is transitive, but delegate's signature is not affected by const transitivity rules - it worked

Re: Ironclad C++

2013-08-06 Thread Kagamin
On Tuesday, 6 August 2013 at 15:13:18 UTC, Kagamin wrote: Ah, an opaque template parameter? It may have value in itself and not require a new syntax or restricted to type qualifiers. Though it must be viral in order to work.

Re: Ironclad C++

2013-08-06 Thread deadalnix
On Tuesday, 6 August 2013 at 15:13:18 UTC, Kagamin wrote: inout already has proper scoping: data external to the function shouldn't be qualified as inout, it just should be checked. In shown examples, 2 function signatures are involved. If you don't understand where the ambiguity lies, I sugge

Re: Ironclad C++

2013-08-06 Thread Timon Gehr
On 08/06/2013 05:13 PM, Kagamin wrote: On Tuesday, 6 August 2013 at 02:11:54 UTC, Timon Gehr wrote: I thought I had demonstrated that it buys you more. It resolves the problem that scoping is ambiguous and that there can be only one 'inout' substitution per function application. It may look am

Re: Ironclad C++

2013-08-09 Thread Kagamin
On Tuesday, 6 August 2013 at 16:55:43 UTC, deadalnix wrote: On Tuesday, 6 August 2013 at 15:13:18 UTC, Kagamin wrote: inout already has proper scoping: data external to the function shouldn't be qualified as inout, it just should be checked. In shown examples, 2 function signatures are involv

Re: Ironclad C++

2013-08-09 Thread Kagamin
On Tuesday, 6 August 2013 at 19:26:09 UTC, Timon Gehr wrote: Nothing subjective about this! Even DMD does not know how the feature works in this case. It's just an unintended implementation error for a case which was not explicitly considered. Should be fixable.

Re: Ironclad C++

2013-08-09 Thread deadalnix
On Friday, 9 August 2013 at 14:47:23 UTC, Kagamin wrote: On Tuesday, 6 August 2013 at 16:55:43 UTC, deadalnix wrote: On Tuesday, 6 August 2013 at 15:13:18 UTC, Kagamin wrote: inout already has proper scoping: data external to the function shouldn't be qualified as inout, it just should be chec

Re: Ironclad C++

2013-08-09 Thread H. S. Teoh
On Fri, Aug 09, 2013 at 07:00:49PM +0200, deadalnix wrote: > On Friday, 9 August 2013 at 14:47:23 UTC, Kagamin wrote: > >On Tuesday, 6 August 2013 at 16:55:43 UTC, deadalnix wrote: > >>On Tuesday, 6 August 2013 at 15:13:18 UTC, Kagamin wrote: > >>>inout already has proper scoping: data external to

Re: Ironclad C++

2013-08-15 Thread Kagamin
On Friday, 9 August 2013 at 17:00:53 UTC, deadalnix wrote: It is ambiguous if the inout of the function passed as parameter stand for the function passed as parameter or the function you pass the parameter to. See my explanation, how inout works and why your example ignores semantics of inout

Re: Ironclad C++

2013-08-15 Thread deadalnix
On Friday, 16 August 2013 at 05:48:12 UTC, Kagamin wrote: On Friday, 9 August 2013 at 17:00:53 UTC, deadalnix wrote: It is ambiguous if the inout of the function passed as parameter stand for the function passed as parameter or the function you pass the parameter to. See my explanation, how i