Ironclad C++

[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" features, like a support for structurally typed
> tuples, that maybe can be designed well enough with the traditional
> method. But perhaps when we/you want to modify/add something in the D
> type system it's better to first find a person able to write down a
> formal proof of soundness of the idea, and only later decide if it's
> worth implementing.

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 am starting to think that to design type system
> features sometimes you need formal mathematics, otherwise you build a
> Swiss cheese.
> ...

This is not only true for type checkers, but for also for other kinds of 
programs. Yet most programming languages do not allow expressing a 
significant amount of checkable non-trivial correctness properties.