On Tuesday, 7 March 2017 at 22:07:51 UTC, XavierAP wrote:
> On Tuesday, 7 March 2017 at 21:24:43 UTC, Moritz Maxeiner wrote:
>> [...]
>
> D does not claim to be memory-safe always.It does afaik do so within @safe environments (barring internal runtime or compiler bugs of course). Even C# has the same approach of allowing "unsafe" environments.

And as I've pointed out before, if your safe code can call hidden, unsafe code it doesn't even know about then your guarantees mean nothing and you're back to trusting programmers.

>
>>>> [...]
>>>
>>> Does anybody try to refute it? Safe languages are not rejected for their safety.
>>
>> Right now, of course not, since the burden of proof is on the side advocating memory safety (i.e. us).
>
> I don't agree on the burden of proof. It is a safe assumption that if you increase safety checks, safety will be improved.

If those safety checks actually get applied to those parts that need them (i.e. by the programmers writing programs in that language), I'd probably agree. But there's no guarantee that that is the case, as your friend, hidden unsafe code, is still there.
Besides that, it's a hypothesis, and like with *all* of them the burden of proof lies with the people proposing/claiming it.

> It cannot or needn't be proven. If someone proposes installing railing in a stairway, or a fence along a railway, to decrease accidents, who would demand this to be proven?

A person with a good sense of engineering (or for that matter the scientific method) in them ought to demand that both your railing, as well as your fence get proven to actually deal with the kinds of issues they are supposed to deal with before approving their installation.
Which is what institutions like [1] are for with regards to material engineering products.
Doing anything else is reckless endangerment since it gives you the feeling of being safe without actually being safe. Like using @safe in D, or Rust, and being unaware of unsafe code hidden from you behind "safe" facades.

>
> Plus statistics can prove nothing -- this logical truth cannot be overstated.

It's called empirical evidence and it's one of the most important techniques in science[2] to create foundation for a hypothesis.

[1] https://en.wikipedia.org/wiki/Technischer_%C3%9Cberwachungsverein
[2] http://www.juliantrubin.com/bigten/millikanoildrop.html

On Sunday, 5 March 2017 at 11:48:23 UTC, Jacob Carlborg wrote:
> On 2017-03-03 16:23, Moritz Maxeiner wrote:
>
>> That would be a good next step from an engineering standpoint, I agree,
>> to proceed to minimize the amount of trust in people you need to have vs
>> verifiable safety.
>> I have considered porting something like seL4[1] to Rust, but ultimately
>> this would take a significant amount of time and even if done you'd then
>> have the biggest problem any new kernel faces: Hardware support. Driver
>> development is AFAIK mostly done by people working for the hardware
>> manufacturer and you're going to have a hard (probably closer to
>> impossible) time convincing them to spend money on driver development
>> for you. And if they don't you'll have close to 30 years of hardware
>> support to catch up on by yourself.
>> But suppose you limit yourself to a single (or at most a handful of
>> homogeneous) platform(s) like [2], e.g. a new AArch64 board. Suppose you
>> even take one where the hardware is open so you can audit its
>> schematics, then you'll *still* either have to use proprietary firmware
>> for the (partially onboard) periphery (and have unsafe interfaces to
>> them), or - once again - write all the device firmware yourself.
>> And once you've done all of that you're still missing userspace, i.e.
>> you have a nice new OS without any actual use for it (yet). So you
>> either start writing your own incompatible, safe userspace, or you're
>> going to decide to integrate the userspace of existing OSs (probably
>> POSIX?) to your new OS, so you're going to be writing your own (safe)
>> libc, (safe) pthread, etc, exposing (once again) unsafe APIs to the top.
>> It will be safer than what we currently have on e.g Linux since you can
>> probably make sure that unsafe use of them won't result in kernel
>> exploits, though; this will, of course, take even more time.
>> Finally, at the arduous end of your journey you're likely going to
>> notice what - in my experience - most new OSs I've observed of the years
>> experience: Essentially nobody is interested in actually switching to a
>> volunteer-based OS.
>> Honestly, I think you need serious corporate backing, a dedicated team,
>> and like 5-10 years (low estimate) of guaranteed development time to
>> have a snowballs chance in hell to pull this off and the only possible
>> sponsors for this I'm both aware of and would currently trust not to cut
>> you off in the middle are either already working on their own OS[3], or
>> have dedicated their R&D to other things[4].
>
> I agree. The only potential hope I see would be to port Linux to a memory safe language.

By Linux, I hope you don't mean the kernel itself. Because outside of being an entirely fruitless venture, it shows a lack of understanding of what's involved in kernel programming.

Most memory safe languages I know don't take well to using bit arithmetic with pointers, deliberately smashing the stack, self modifying code, and a whole plethora of things required to work with the CPU in a freestanding environment. Within the span of a single function call, an address in memory is easily able to refer to a different address on physical memory.

Forgive me if I'm wrong, but I don't think you can get that much benefit out of memory safety when you change the address of the stack pointer manually and start to manually prefill it with new values for general registers.

On Wednesday, 8 March 2017 at 12:42:37 UTC, Moritz Maxeiner wrote:
> On Tuesday, 7 March 2017 at 22:07:51 UTC, XavierAP wrote:
>> Plus statistics can prove nothing -- this logical truth cannot be overstated.
>
> It's called empirical evidence and it's one of the most important techniques in science[2] to create foundation for a hypothesis.

No, mistaking historical data as empirically valid is the most dangerous scientific mistake. The empirical method requires all conditions to be controlled, in order for factors to be isolated, and every experiment to be reproducible.

On Wednesday, 8 March 2017 at 12:42:37 UTC, Moritz Maxeiner wrote:
> Doing anything else is reckless endangerment since it gives you the feeling of being safe without actually being safe. Like using @safe in D, or Rust, and being unaware of unsafe code hidden from you behind "safe" facades.

Safe code should be unable to call unsafe code -- including interop with any non-D or binary code, here I agree. I was supposing this is already the case in D but I'm not really sure.

On Wednesday, 8 March 2017 at 13:12:12 UTC, Minty Fresh wrote:
> On Sunday, 5 March 2017 at 11:48:23 UTC, Jacob Carlborg wrote:
>> On 2017-03-03 16:23, Moritz Maxeiner wrote:
>>
>>> That would be a good next step from an engineering standpoint, I agree,
>>> to proceed to minimize the amount of trust in people you need to have vs
>>> verifiable safety.
>>> I have considered porting something like seL4[1] to Rust, but ultimately
>>> this would take a significant amount of time and even if done you'd then
>>> have the biggest problem any new kernel faces: Hardware support. Driver
>>> development is AFAIK mostly done by people working for the hardware
>>> manufacturer and you're going to have a hard (probably closer to
>>> impossible) time convincing them to spend money on driver development
>>> for you. And if they don't you'll have close to 30 years of hardware
>>> support to catch up on by yourself.
>>> But suppose you limit yourself to a single (or at most a handful of
>>> homogeneous) platform(s) like [2], e.g. a new AArch64 board. Suppose you
>>> even take one where the hardware is open so you can audit its
>>> schematics, then you'll *still* either have to use proprietary firmware
>>> for the (partially onboard) periphery (and have unsafe interfaces to
>>> them), or - once again - write all the device firmware yourself.
>>> And once you've done all of that you're still missing userspace, i.e.
>>> you have a nice new OS without any actual use for it (yet). So you
>>> either start writing your own incompatible, safe userspace, or you're
>>> going to decide to integrate the userspace of existing OSs (probably
>>> POSIX?) to your new OS, so you're going to be writing your own (safe)
>>> libc, (safe) pthread, etc, exposing (once again) unsafe APIs to the top.
>>> It will be safer than what we currently have on e.g Linux since you can
>>> probably make sure that unsafe use of them won't result in kernel
>>> exploits, though; this will, of course, take even more time.
>>> Finally, at the arduous end of your journey you're likely going to
>>> notice what - in my experience - most new OSs I've observed of the years
>>> experience: Essentially nobody is interested in actually switching to a
>>> volunteer-based OS.
>>> Honestly, I think you need serious corporate backing, a dedicated team,
>>> and like 5-10 years (low estimate) of guaranteed development time to
>>> have a snowballs chance in hell to pull this off and the only possible
>>> sponsors for this I'm both aware of and would currently trust not to cut
>>> you off in the middle are either already working on their own OS[3], or
>>> have dedicated their R&D to other things[4].
>>
>> I agree. The only potential hope I see would be to port Linux to a memory safe language.
>
> By Linux, I hope you don't mean the kernel itself. Because outside of being an entirely fruitless venture, it shows a lack of understanding of what's involved in kernel programming.
>
> Most memory safe languages I know don't take well to using bit arithmetic with pointers, deliberately smashing the stack, self modifying code, and a whole plethora of things required to work with the CPU in a freestanding environment. Within the span of a single function call, an address in memory is easily able to refer to a different address on physical memory.
>
> Forgive me if I'm wrong, but I don't think you can get that much benefit out of memory safety when you change the address of the stack pointer manually and start to manually prefill it with new values for general registers.

I will just leave this here.

https://muen.codelabs.ch/

On Wednesday, 8 March 2017 at 13:30:42 UTC, XavierAP wrote:
> On Wednesday, 8 March 2017 at 12:42:37 UTC, Moritz Maxeiner wrote:
>> Doing anything else is reckless endangerment since it gives you the feeling of being safe without actually being safe. Like using @safe in D, or Rust, and being unaware of unsafe code hidden from you behind "safe" facades.
>
> Safe code should be unable to call unsafe code -- including interop with any non-D or binary code, here I agree. I was supposing this is already the case in D but I'm not really sure.

You can hide unsafe code in D by annotating a function with @trusted the same way you can hide unsafe code in Rust with unsafe blocks.

On Wednesday, 8 March 2017 at 13:14:19 UTC, XavierAP wrote:
> On Wednesday, 8 March 2017 at 12:42:37 UTC, Moritz Maxeiner wrote:
>> On Tuesday, 7 March 2017 at 22:07:51 UTC, XavierAP wrote:
>>> Plus statistics can prove nothing -- this logical truth cannot be overstated.
>>
>> It's called empirical evidence and it's one of the most important techniques in science[2] to create foundation for a hypothesis.
>
> No, mistaking historical data as empirically valid is the most dangerous scientific mistake. The empirical method requires all conditions to be controlled, in order for factors to be isolated, and every experiment to be reproducible.

This is true for controlled experiments like the one I pointed to and this model works fine for those sciences where controlled experiments are applicable (e.g. physics).
For (soft) sciences where human behaviour is a factor - and it usually is one you cannot reliably control - using quasi-experiments with a high sample size is a generally accepted practice to accumulate empirical data.

On Wednesday, 8 March 2017 at 13:50:28 UTC, Paulo Pinto wrote:
> [...]
>
> I will just leave this here.
>
> https://muen.codelabs.ch/

This seems really cool, but I though seL4[1] were the first in the field.
Guess I'll have some more research to do :p

[1] https://sel4.systems/

On Wednesday, 8 March 2017 at 14:02:40 UTC, Moritz Maxeiner wrote:
> On Wednesday, 8 March 2017 at 13:14:19 UTC, XavierAP wrote:
>> On Wednesday, 8 March 2017 at 12:42:37 UTC, Moritz Maxeiner wrote:
>>> On Tuesday, 7 March 2017 at 22:07:51 UTC, XavierAP wrote:
>>>> Plus statistics can prove nothing -- this logical truth cannot be overstated.
>>>
>>> It's called empirical evidence and it's one of the most important techniques in science[2] to create foundation for a hypothesis.
>>
>> No, mistaking historical data as empirically valid is the most dangerous scientific mistake. The empirical method requires all conditions to be controlled, in order for factors to be isolated, and every experiment to be reproducible.
>
> This is true for controlled experiments like the one I pointed to and this model works fine for those sciences where controlled experiments are applicable (e.g. physics).
> For (soft) sciences where human behaviour is a factor - and it usually is one you cannot reliably control - using quasi-experiments with a high sample size is a generally accepted practice to accumulate empirical data.

Right, but that's why "soft" sciences that use any "soft" version of the empirical method, have no true claim to being actual sciences. And it's why whenever you don't like an economist's opinion, you can easily find another with the opposite opinion and his own model.

There are other sane approaches for "soft" sciences where (controlled) experiments aren't possible:

https://en.wikipedia.org/wiki/Praxeology#Origin_and_etymology

Of course these methods have limits on what can be inferred, whereas with models tuned onto garbage historical statistics you can keep publishing to scientific journals forever, and never reach any incontestable conclusion.

On Wednesday, 8 March 2017 at 14:50:18 UTC, XavierAP wrote:
> On Wednesday, 8 March 2017 at 14:02:40 UTC, Moritz Maxeiner wrote:
>> [...]
>>
>> This is true for controlled experiments like the one I pointed to and this model works fine for those sciences where controlled experiments are applicable (e.g. physics).
>> For (soft) sciences where human behaviour is a factor - and it usually is one you cannot reliably control - using quasi-experiments with a high sample size is a generally accepted practice to accumulate empirical data.
>
> Right, but that's why "soft" sciences that use any "soft" version of the empirical method, have no true claim to being actual sciences.

That is an opinion, though; same as my initial position that enough empirical data about whether people in memory safe languages (but where your safe code can call hidden unsafe code without you knowing it) actually end up creating memory safe programs could provide enough foundation to exclaim "I told you so" if it turns out that the discrepancy is significant enough (what significant means in this context is, of course, another opinion).

> And it's why whenever you don't like an economist's opinion, you can easily find another with the opposite opinion and his own model.

I'm not an economist and can neither speak to the assumptions in this, nor the conclusion.

>
> There are other sane approaches for "soft" sciences where (controlled) experiments aren't possible:
>
> https://en.wikipedia.org/wiki/Praxeology#Origin_and_etymology
>
> Of course these methods have limits on what can be inferred, whereas with models tuned onto garbage historical statistics you can keep publishing to scientific journals forever, and never reach any incontestable conclusion.

Thank you, I'll put praxeology on my list of things to read up on.