On 10/4/2014 3:30 AM, Steven Schveighoffer wrote:
> On 10/4/14 4:47 AM, Walter Bright wrote:
>> On 9/29/2014 8:13 AM, Steven Schveighoffer wrote:
>>> I can think of cases where it's programmer error, and cases where it's
>>> user error.
>>
>> More carefully design the interfaces if programmer error and input error
>> are conflated.
>>
>
> You mean more carefully design File's ctor? How so?

You can start with deciding if random  binary data passed as a "file name" is legal input to the ctor or not.

On Saturday, 4 October 2014 at 11:39:24 UTC, Joseph Rushton Wakeling wrote:
> The thing is, the privilege to make that kind of business decision is wholly dependent on the fact that there are no meaningful safety issues involved.

Surgeons can do remote surgery using VR equipment. There are obvious dangerous technical factors there, but you have to weigh that up to getting an emergency operation done by the most exerienced surgeon in the country. So it is a probabilistic calculation. From an absolute safety point of view, you should not do that. The comm link might fail and that could be serious. It is a system that might create extra complications. From a probabilistic point of view it might lead to the highest survial rate and make local surgeons better, so it might be worth the risk when you amortize risk over N operations.

On Saturday, 4 October 2014 at 19:49:23 UTC, Walter Bright wrote:
> On 10/4/2014 7:13 AM, H. S. Teoh via Digitalmars-d wrote:
>> "Beware -- I've only proven that the code is correct, not tested it." --
>> Donald Knuth.
>>
>> :-)
>
> Quotes like that prove (!) what a cool guy Knuth is!

Nah, it only proves that he had not tested the code in his memo (and probably not run the proof through a verifier either).

On 10/04/2014 10:37 PM, Ola Fosheim Grostad wrote:
> On Saturday, 4 October 2014 at 19:49:23 UTC, Walter Bright wrote:
>> On 10/4/2014 7:13 AM, H. S. Teoh via Digitalmars-d wrote:
>>> "Beware -- I've only proven that the code is correct, not tested it." --
>>> Donald Knuth.
>>>
>>> :-)
>>
>> Quotes like that prove (!) what a cool guy Knuth is!
>
> Nah, it only proves that he had not tested the code in his memo (and
> probably not run the proof through a verifier either).

It doesn't prove that.

On 09/28/2014 04:13 PM, Walter Bright wrote:
>
> A program bug is, by definition, unknown and unanticipated. The idea
> that one can "recover" from it is fundamentally wrong.

In many cases you can. Don't forget, enterprise code aside, we're not in the days of spaghetti code where everything's directly intermingled: Things are encapsulated. If I call on a component, and that component fails, chances are the problems exist purely within that component. So yes, recovery is most definitely possible. Not *always*, but often.

I imagine you're about to jump on that "chances are" and "not always" part...and you're right: For safety-critical software, relying on that "*chances are*" the bug exists purely within that component is, of course, completely inappropriate. I won't dispute that.

But a LOT of software is *NOT* safety-critical. In those cases, going through the trouble of process-separated components or complete shutdowns on every minor compartmentalized hiccup, just on the off-chance that it might be symptomatic of something bigger (it usually isn't) usually amounts to swatting a fly with a bazooka.

If tetris, or "semi-interactive movie of the year", or a music library manager, or an online poll, or youtube comments suddenly goes haywire, it's really not a big deal. And process separation and permissions still limit the collateral damage anyway. It's unprofessional, sure, all bugs and crashes are, but it's certainly no less professional than a program that shuts down whenever the digital wind shifts.

Also, on a somewhat separate note:

As other have indicted, suppose you *do* strictly limit Exceptions to bad user inputs and other expected non-logic-errors. What happens when you forget to handle one of those Exceptions? That's a logic error that manifests as an uncaught Exception.

Code that handles and recovers from bad user input and other such "Exception" purposes is every bit as subject to logic errors as any other code. Therefore it is *impossible* to reliably ensure that Exception *only* indicates non-logic-errors such as bad user input. So the whole notion of strict separation falls apart right there. Exceptions are *going to* occasionally indicate logic errors, period. Therefore, they must carry enough information to help the developer diagnose and fix.

Is showing that diagnostic information to the user upon a crash unprofessional? Sure. But *all* crashes are unprofessional, so there's really no avoiding that. The *least* unprofessional crashes are the ones that 1. Don't get triggered more often than actually necessary (considering the given program domain.) and 2. Contain enough information to actually get fixed.

On 10/3/14, 9:26 PM, ketmar via Digitalmars-d wrote:
> yes. DMD attempts to 'guess' what identifier i mistyped drives me
> crazy. just shut up and stop after "unknown identifier", you robot,
> don't try to show me your artificial idiocity!

awesome feature -- Andrei

On 10/04/2014 03:57 PM, Ola Fosheim Grostad wrote:
>
> A validated correctness proof ensures that the code follows the
> specification, so no bugs.
>

The day we can guarantee a correctness proof as being perfectly sound and...well...correct is the day we can guarantee software correctness without the formal proof.

Proofs are just as subject to mistakes and oversights as actual code. Proofs deal with that via auditing and peer review, but...so does software. It sure as hell doesn't guarantee lack of bugs in software, so what in the world would make anyone think it magically guarantees lack of mistakes in a "proof"? (A "proof" btw, is little more than code which may or may not ever actually get mechanically executed.)

On 10/04/2014 06:20 PM, Nick Sabalausky wrote:
> On 10/04/2014 03:57 PM, Ola Fosheim Grostad wrote:
>>
>> A validated correctness proof ensures that the code follows the
>> specification, so no bugs.
>>
>
> The day we can guarantee a correctness proof as being perfectly sound
> and...well...correct is the day we can guarantee software correctness
> without the formal proof.
>
> Proofs are just as subject to mistakes and oversights as actual code.
> Proofs deal with that via auditing and peer review, but...so does
> software. It sure as hell doesn't guarantee lack of bugs in software, so
> what in the world would make anyone think it magically guarantees lack
> of mistakes in a "proof"? (A "proof" btw, is little more than code which
> may or may not ever actually get mechanically executed.)
>

And the "specification" itself may have flaws as well, so again, there are NO guarantees here whatsoever. The only thing proofs do in an engineering context is decrease the likelihood of problems, just like any other engineering strategy.

On 10/4/2014 3:24 PM, Nick Sabalausky wrote:
> On 10/04/2014 06:20 PM, Nick Sabalausky wrote:
>> The day we can guarantee a correctness proof as being perfectly sound
>> and...well...correct is the day we can guarantee software correctness
>> without the formal proof.
>>
>> Proofs are just as subject to mistakes and oversights as actual code.
>> Proofs deal with that via auditing and peer review, but...so does
>> software. It sure as hell doesn't guarantee lack of bugs in software, so
>> what in the world would make anyone think it magically guarantees lack
>> of mistakes in a "proof"? (A "proof" btw, is little more than code which
>> may or may not ever actually get mechanically executed.)
>>
>
> And the "specification" itself may have flaws as well, so again, there are NO
> guarantees here whatsoever. The only thing proofs do in an engineering context
> is decrease the likelihood of problems, just like any other engineering strategy.


Yup. Proofs are just another tool that helps, not a magic solution.

On 10/4/2014 2:45 PM, Andrei Alexandrescu wrote:
> On 10/3/14, 9:26 PM, ketmar via Digitalmars-d wrote:
>> yes. DMD attempts to 'guess' what identifier i mistyped drives me
>> crazy. just shut up and stop after "unknown identifier", you robot,
>> don't try to show me your artificial idiocity!
>
> awesome feature -- Andrei

I agree, I like it very much.