www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - D for safety critical applications

reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
Talking with some colleges. They have some questions regarding D:

1. Is D ready for prime time á la safety critical applications?
(I guess they mean GDC on ARM for example)

2. Are there any plans to make a certified compiler?
Feb 08 2021
next sibling parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?


What kind of safety critical applications are we talking about? 
Which certifications are you targeting for your product(s)?

I'm not currently aware of any certified compilers for D. It 
would be cool if one existed, though.
Feb 08 2021
parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Monday, 8 February 2021 at 11:19:44 UTC, Gregor Mückl wrote:

 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?


 What kind of safety critical applications are we talking about? 
 Which certifications are you targeting for your product(s)?

 I'm not currently aware of any certified compilers for D. It 
 would be cool if one existed, though.


I'm in a bit of a hurry atm, but basically IEC 61508 and ISO 
26262 (we have older systems for EN 50128 and EN 50657 but they 
are not actively developed):

https://www.iar.com/iar-embedded-workbench/certified-tools-for-functional-safety/
Feb 08 2021
parent reply Denis Feklushkin <feklushkin.denis gmail.com> writes:
On Monday, 8 February 2021 at 13:17:31 UTC, Imperatorn wrote:


 What kind of safety critical applications are we talking 
 about? Which certifications are you targeting for your 
 product(s)?

 I'm not currently aware of any certified compilers for D. It 
 would be cool if one existed, though.


 I'm in a bit of a hurry atm, but basically IEC 61508 and ISO 
 26262 (we have older systems for EN 50128 and EN 50657 but they 
 are not actively developed):

 https://www.iar.com/iar-embedded-workbench/certified-tools-for-functional-safety/


In brief, how does it work? If a bug will be found in the 
compiler, certifying authority (or its staff) will be fined?
Feb 08 2021
parent Dominikus Dittes Scherkl <dominikus scherkl.de> writes:
On Monday, 8 February 2021 at 23:01:17 UTC, Denis Feklushkin 
wrote:

 On Monday, 8 February 2021 at 13:17:31 UTC, Imperatorn wrote:


 What kind of safety critical applications are we talking 
 about? Which certifications are you targeting for your 
 product(s)?

 I'm not currently aware of any certified compilers for D. It 
 would be cool if one existed, though.


 I'm in a bit of a hurry atm, but basically IEC 61508 and ISO 
 26262 (we have older systems for EN 50128 and EN 50657 but 
 they are not actively developed):

 https://www.iar.com/iar-embedded-workbench/certified-tools-for-functional-safety/


 In brief, how does it work? If a bug will be found in the 
 compiler, certifying authority (or its staff) will be fined?


The certification only increases the trust in a SW generated by 
the certified tool.
Without this certificate a tool is simply not allowed to be used 
to build ISO compliant SW.
But the SW still need to be fully tested and the tool provider is 
not responsible for any undetected bug in the resulting SW.
Of course a tool bug need to be documented, if its vendor wants 
to keep its certification. It is not even a fix required, not to 
mention fines :-)
Feb 09 2021
prev sibling next sibling parent reply Paulo Pinto <pjmlp progtools.org> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?


Besides C and C++, I am only aware of Java (PTC/Aicas) and Ada 
compilers as fully certified compilers.

Rust has one company driving the roadmap for such kind of 
deployments,

https://ferrous-systems.com/blog/sealed-rust-the-pitch/

Whereas Wilderness Labs is driving .NET IoT efforts, however 
without certification in place,

https://www.wildernesslabs.co/

I am not aware of similar efforts regarding D.
Feb 08 2021
parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Monday, 8 February 2021 at 15:12:47 UTC, Paulo Pinto wrote:

 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?


 Besides C and C++, I am only aware of Java (PTC/Aicas) and Ada 
 compilers as fully certified compilers.

 Rust has one company driving the roadmap for such kind of 
 deployments,

 https://ferrous-systems.com/blog/sealed-rust-the-pitch/

 Whereas Wilderness Labs is driving .NET IoT efforts, however 
 without certification in place,

 https://www.wildernesslabs.co/

 I am not aware of similar efforts regarding D.


We might not need the compiler to be certified if we can do other 
tests (like using Klee etc). But was curious if it had been 
discussed before.
Feb 08 2021
parent rikki cattermole <rikki cattermole.co.nz> writes:
On 09/02/2021 4:44 AM, Imperatorn wrote:

 We might not need the compiler to be certified if we can do other tests 
 (like using Klee etc). But was curious if it had been discussed before.


Walter has said, that we won't do certification without a reason.
Once we have a reason such as your company we can determine what needs 
to be done, and do it.

The next step is to talk to him I think.
Feb 08 2021
prev sibling next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 2/8/2021 3:09 AM, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding D:
 
 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)


Sure. It's far better than C is. The biggest impact is simply having array 
overflow detection. There's a lot more, too, such as protections against 
uninitialized variables and pointers to expired stack frames.



 2. Are there any plans to make a certified compiler?


Not at the moment.
Feb 09 2021
next sibling parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Tuesday, 9 February 2021 at 09:39:50 UTC, Walter Bright wrote:

 On 2/8/2021 3:09 AM, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:
 
 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)


 Sure. It's far better than C is. The biggest impact is simply 
 having array overflow detection. There's a lot more, too, such 
 as protections against uninitialized variables and pointers to 
 expired stack frames.



 2. Are there any plans to make a certified compiler?


 Not at the moment.


Splendid! I'll try to convince my colleagues to try it 🐢
Feb 09 2021
prev sibling parent reply Lasheen <hazem.lasheen yandex.com> writes:
On Tuesday, 9 February 2021 at 09:39:50 UTC, Walter Bright wrote:

 On 2/8/2021 3:09 AM, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:
 
 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)


 Sure. It's far better than C is. The biggest impact is simply 
 having array overflow detection. There's a lot more, too, such 
 as protections against uninitialized variables and pointers to 
 expired stack frames.



 2. Are there any plans to make a certified compiler?


 Not at the moment.


where i can find a detailed tutorial that can help me to 
understand how to use D
in AI apps and specially when mission-critical system is needed.
Mar 16 2021
next sibling parent rikki cattermole <rikki cattermole.co.nz> writes:
On 17/03/2021 4:30 PM, Lasheen wrote:

 where i can find a detailed tutorial that can help me to understand how 
 to use D
 in AI apps and specially when mission-critical system is needed.


There are no tutorials.

You may find it is easier to ask the questions you have over on Discord.

https://discord.gg/VRg3CeqD
Mar 16 2021
prev sibling parent reply Dukc <ajieskola gmail.com> writes:
On Wednesday, 17 March 2021 at 03:30:17 UTC, Lasheen wrote:

 where i can find a detailed tutorial that can help me to 
 understand how to use D
 in AI apps and specially when mission-critical system is needed.


Not a tutorial, but Walter has written many articles that should 
hint towards the right mindset: 
https://digitalmars.com/articles/index.html

Mission-critical systems are something I feel it is terribly 
difficult to find tutorials on. In any language, not just in D. 
One can learn by watching by following development of critical 
open-source projects - OpenSSL, Tor or different Unix kernels for 
example. But other than them, I feel critical systems design is 
an art that tends be locked in the proprietary world - correct me 
if I'm wrong.
Mar 17 2021
parent Paulo Pinto <pjmlp progtools.org> writes:
On Wednesday, 17 March 2021 at 21:37:01 UTC, Dukc wrote:

 On Wednesday, 17 March 2021 at 03:30:17 UTC, Lasheen wrote:

 where i can find a detailed tutorial that can help me to 
 understand how to use D
 in AI apps and specially when mission-critical system is 
 needed.


 Not a tutorial, but Walter has written many articles that 
 should hint towards the right mindset: 
 https://digitalmars.com/articles/index.html

 Mission-critical systems are something I feel it is terribly 
 difficult to find tutorials on. In any language, not just in D. 
 One can learn by watching by following development of critical 
 open-source projects - OpenSSL, Tor or different Unix kernels 
 for example. But other than them, I feel critical systems 
 design is an art that tends be locked in the proprietary world 
 - correct me if I'm wrong.


That knowledge is available if one searches for it.

https://www.perforce.com/resources/qac/misra-c-cpp

https://frama-c.com/

https://www.rapitasystems.com/downloads/validation-cots-ada-compiler-safety-critical-applications

https://www.amazon.com/Real-Time-Critical-Systems-Prototype-Integration/dp/1984171992

https://dl.acm.org/doi/10.5555/111797.111813
Mar 18 2021
prev sibling next sibling parent reply IGotD- <nise nise.com> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?


Just to put it into some perspective. I have worked with so 
called certified C/C++ compilers in the automotive industry. I 
remember encountered several bugs in those compilers as well they 
are usually far behind when adopting the new language standards. 
Compare this to GCC, when was the last time you encountered a bug 
in that compiler? I can't remember any.

The certified compilers which are not better than GCC are usually 
proprietary and cost money for each user. Here we have a product 
that is essentially worse than GCC and cost money. What it is 
really about is a form of corruption. The only positive side is 
that if you find a bug you can put pressure on the company that 
provides the compiler but usually that takes several months.
Feb 09 2021
next sibling parent reply Dominikus Dittes Scherkl <dominikus scherkl.de> writes:
On Tuesday, 9 February 2021 at 10:10:05 UTC, IGotD- wrote:

 Just to put it into some perspective. I have worked with so 
 called certified C/C++ compilers in the automotive industry. I 
 remember encountered several bugs in those compilers as well 
 they are usually far behind when adopting the new language 
 standards.


As I said, fixing bugs is NOT required for certification.
It is only necessary to document them.


 The certified compilers which are not better than GCC are 
 usually proprietary and cost money for each user.


You can qualify a tool to be used in an ISO compliant build 
process on your own (in your company). We do this regularly for 
every little script we use. But to qualify something as complex 
as a compiler is a huge lot of work.
This is why getting an official certificate (from e.g. TÜV) is so 
expensive that a vendor NEEDS to sell it and can't give it away 
for free.


 Here we have a product that is essentially worse than GCC and 
 cost money. What it is really about is a form of corruption.


Harsh words.
If you don't want to pay for a compiler, qualify it yourself. 
You'll see it cost you at least the same amount of money (or 
time).


 Compare this to GCC, when was the last time you encountered a 
 bug in that compiler? I can't remember any.


But this is only because also there the bugs are quiet good 
documented in bugzilla and so can easily be avoided.
Having this documentation will help you a lot in qualifying the 
compiler yourself.
Feb 09 2021
parent reply Bastiaan Veelo <Bastiaan Veelo.net> writes:
On Tuesday, 9 February 2021 at 11:25:26 UTC, Dominikus Dittes 
Scherkl wrote:

 As I said, fixing bugs is NOT required for certification.
 It is only necessary to document them.


Out of curiosity, what happens next then? I assume the goal is to 
certify your application. In the process of certifying your 
application, wouldn't you have to prove that the application does 
not trigger any of the documented bugs in the certified tools? 
This could well be harder to do than fixing the bugs in the tools.

-- Bastiaan.
Feb 09 2021
parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Tuesday, 9 February 2021 at 12:38:21 UTC, Bastiaan Veelo wrote:

 On Tuesday, 9 February 2021 at 11:25:26 UTC, Dominikus Dittes 
 Scherkl wrote:

 As I said, fixing bugs is NOT required for certification.
 It is only necessary to document them.


 Out of curiosity, what happens next then? I assume the goal is 
 to certify your application. In the process of certifying your 
 application, wouldn't you have to prove that the application 
 does not trigger any of the documented bugs in the certified 
 tools? This could well be harder to do than fixing the bugs in 
 the tools.

 -- Bastiaan.


I'm not aware that any certification requires explicit proof that 
you avoid those bugs. This is mostly covered indirectly by two 
things: you need to adhere to the safety manual for the tools you 
use and you need a pretty rigorous testing regime for your 
product. The mandated test coverage should be good enough to 
detect misbehaving code introduced by faulty tools.
Feb 09 2021
parent reply Bastiaan Veelo <Bastiaan Veelo.net> writes:
On Tuesday, 9 February 2021 at 13:22:22 UTC, Gregor Mückl wrote:

 On Tuesday, 9 February 2021 at 12:38:21 UTC, Bastiaan Veelo 
 wrote:

 On Tuesday, 9 February 2021 at 11:25:26 UTC, Dominikus Dittes 
 Scherkl wrote:

 As I said, fixing bugs is NOT required for certification.
 It is only necessary to document them.


 Out of curiosity, what happens next then? I assume the goal is 
 to certify your application. In the process of certifying your 
 application, wouldn't you have to prove that the application 
 does not trigger any of the documented bugs in the certified 
 tools? This could well be harder to do than fixing the bugs in 
 the tools.

 -- Bastiaan.


 I'm not aware that any certification requires explicit proof 
 that you avoid those bugs. This is mostly covered indirectly by 
 two things: you need to adhere to the safety manual for the 
 tools you use and you need a pretty rigorous testing regime for 
 your product. The mandated test coverage should be good enough 
 to detect misbehaving code introduced by faulty tools.


This makes me wonder what certifying the tool practically brings 
to the table, apart from doors that can be entered with a 
certificate only. If certification of the tool does not improve 
the safety of the product and does not make it easier to test the 
safety of the product, I have the feeling that the certificate 
only improves perceived safety.

Your other comment that the certified commercial compiler you 
used produced higher quality binaries is not necessarily due to 
the certification, but likely due to available funds.

-- Bastiaan.
Feb 09 2021
next sibling parent reply Dominikus Dittes Scherkl <dominikus scherkl.de> writes:
On Tuesday, 9 February 2021 at 14:14:42 UTC, Bastiaan Veelo wrote:

 On Tuesday, 9 February 2021 at 13:22:22 UTC, Gregor Mückl wrote:



 I'm not aware that any certification requires explicit proof 
 that you avoid those bugs.[...]


 This makes me wonder what certifying the tool practically 
 brings to the table, apart from doors that can be entered with 
 a certificate only.


Nothing. It's a key to some doors. If you like to enter them, you 
have to have the key. It's the same as with every certificate.
E.g. if you don't have a CE-certificate, you can't sell your 
product in the EU.
If you don't have the ISO-certificate, can't sell your controller 
software to a major vendor.


 If certification of the tool does not improve the safety of the 
 product and does not make it easier to test the safety of the 
 product, I have the feeling that the certificate only improves 
 perceived safety.


No, the certificate ensures that someone put intense thoughts 
about safety into the tool and documented what usecases it is 
good for and what you need to avoid to create a safe product with 
it. Thoughts that you would have to do yourself if you use a tool 
without that certificate.

I know, here are a lot of people that have very little trust in 
thoughts that someone else put into something, but it's their 
choice: use something certified or spent a lot of time to prove 
it yourself.
If you proof it yourself anyway, a certificate maybe really 
useless for you.
Feb 09 2021
parent reply FeepingCreature <feepingcreature gmail.com> writes:
On Tuesday, 9 February 2021 at 15:10:55 UTC, Dominikus Dittes 
Scherkl wrote:

 I know, here are a lot of people that have very little trust in 
 thoughts that someone else put into something, but it's their 
 choice: use something certified or spent a lot of time to prove 
 it yourself.
 If you proof it yourself anyway, a certificate maybe really 
 useless for you.


I don't see how a certificate relieves you of the responsibility 
to consider the safety and quality of your tools yourself.

You use a certified compiler. The certified compiler produces a 
bug. As a result, a product that you released doesn't work. Does 
that mean that it isn't your problem? No, of course it doesn't! 
It's still 100% on you to fix it. With that said, I don't 
understand what you are paying for. Are you paying for the vendor 
to think about security? But why would you want to use a tool 
from a vendor who doesn't think about security to begin with? One 
way or another, the buck stops with you, not the vendor.

It's not that if you consider the safety and security of your 
tools yourself, the certificate is useless for you. It's that you 
have to consider the safety and security of your tools *whether 
or not* they're certified.
Feb 09 2021
next sibling parent Paul Backus <snarwin gmail.com> writes:
On Tuesday, 9 February 2021 at 15:37:42 UTC, FeepingCreature 
wrote:

 On Tuesday, 9 February 2021 at 15:10:55 UTC, Dominikus Dittes 
 Scherkl wrote:

 I know, here are a lot of people that have very little trust 
 in thoughts that someone else put into something, but it's 
 their choice: use something certified or spent a lot of time 
 to prove it yourself.
 If you proof it yourself anyway, a certificate maybe really 
 useless for you.


 I don't see how a certificate relieves you of the 
 responsibility to consider the safety and quality of your tools 
 yourself.

 You use a certified compiler. The certified compiler produces a 
 bug. As a result, a product that you released doesn't work. 
 Does that mean that it isn't your problem? No, of course it 
 doesn't! It's still 100% on you to fix it. With that said, I 
 don't understand what you are paying for. Are you paying for 
 the vendor to think about security? But why would you want to 
 use a tool from a vendor who doesn't think about security to 
 begin with? One way or another, the buck stops with you, not 
 the vendor.


Probably if somebody attempts to sue you for negligence, you will 
be in a better position to defend yourself if you can show that 
you used a certified compiler than if you used something like GCC 
or Clang. So what you are paying for is for the vendor to assume 
some (though not all) of the risk of blame if your product has a 
defect. In other words, the certificate is an insurance policy.
Feb 09 2021
prev sibling parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Tuesday, 9 February 2021 at 15:37:42 UTC, FeepingCreature 
wrote:

 On Tuesday, 9 February 2021 at 15:10:55 UTC, Dominikus Dittes 
 Scherkl wrote:

 I know, here are a lot of people that have very little trust 
 in thoughts that someone else put into something, but it's 
 their choice: use something certified or spent a lot of time 
 to prove it yourself.
 If you proof it yourself anyway, a certificate maybe really 
 useless for you.


 I don't see how a certificate relieves you of the 
 responsibility to consider the safety and quality of your tools 
 yourself.

 You use a certified compiler. The certified compiler produces a 
 bug. As a result, a product that you released doesn't work. 
 Does that mean that it isn't your problem? No, of course it 
 doesn't! It's still 100% on you to fix it. With that said, I 
 don't understand what you are paying for. Are you paying for 
 the vendor to think about security? But why would you want to 
 use a tool from a vendor who doesn't think about security to 
 begin with? One way or another, the buck stops with you, not 
 the vendor.


I think there is a slight misconception in this thread that the 
certification is for the end product only when it is focused a 
lot on the processes that result in it. That also means that the 
vendor providing a certified product is under certain 
obligations. One of them is enabling the user of the tool to use 
it properly (e.g. a safety manual), another one is an obligation 
to manage defects. AFAIK this involves a process for notifying 
customers of critical bugs.

Nitpick: safety != security. Safety in this context means that 
the resulting product does not experience silent or undetected 
malfunctions. Security is resilience towards dedicated attacks on 
a system. These are different things, even though they overlap to 
some degree.

The reality is that a lot of ISO 61508 compliant environments are 
safe (i.e. the factory *will* shut down safely if things break), 
but terribly insecure (a hacker can take over and mess with tons 
of parameters).


 It's not that if you consider the safety and security of your 
 tools yourself, the certificate is useless for you. It's that 
 you have to consider the safety and security of your tools 
 *whether or not* they're certified.


This. You need to invest considerable time and effort to 
establish processes and toolchains that are compliant. A tool 
certificate is no good if the processes around it are not 
compliant. There are many ways in which you can be non-compliant 
with a compliant toolchain. The impact of a certificate on your 
own processes is simply that tool qualification has already 
happened elsewhere.
Feb 09 2021
parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Tuesday, 9 February 2021 at 16:58:35 UTC, Gregor Mückl wrote:

 On Tuesday, 9 February 2021 at 15:37:42 UTC, FeepingCreature 
 wrote:

 On Tuesday, 9 February 2021 at 15:10:55 UTC, Dominikus Dittes 
 Scherkl wrote:

 I know, here are a lot of people that have very little trust 
 in thoughts that someone else put into something, but it's 
 their choice: use something certified or spent a lot of time 
 to prove it yourself.
 If you proof it yourself anyway, a certificate maybe really 
 useless for you.


 I don't see how a certificate relieves you of the 
 responsibility to consider the safety and quality of your 
 tools yourself.

 You use a certified compiler. The certified compiler produces 
 a bug. As a result, a product that you released doesn't work. 
 Does that mean that it isn't your problem? No, of course it 
 doesn't! It's still 100% on you to fix it. With that said, I 
 don't understand what you are paying for. Are you paying for 
 the vendor to think about security? But why would you want to 
 use a tool from a vendor who doesn't think about security to 
 begin with? One way or another, the buck stops with you, not 
 the vendor.


 I think there is a slight misconception in this thread that the 
 certification is for the end product only when it is focused a 
 lot on the processes that result in it. That also means that 
 the vendor providing a certified product is under certain 
 obligations. One of them is enabling the user of the tool to 
 use it properly (e.g. a safety manual), another one is an 
 obligation to manage defects. AFAIK this involves a process for 
 notifying customers of critical bugs.

 Nitpick: safety != security. Safety in this context means that 
 the resulting product does not experience silent or undetected 
 malfunctions. Security is resilience towards dedicated attacks 
 on a system. These are different things, even though they 
 overlap to some degree.

 The reality is that a lot of ISO 61508 compliant environments 
 are safe (i.e. the factory *will* shut down safely if things 
 break), but terribly insecure (a hacker can take over and mess 
 with tons of parameters).


 It's not that if you consider the safety and security of your 
 tools yourself, the certificate is useless for you. It's that 
 you have to consider the safety and security of your tools 
 *whether or not* they're certified.


 This. You need to invest considerable time and effort to 
 establish processes and toolchains that are compliant. A tool 
 certificate is no good if the processes around it are not 
 compliant. There are many ways in which you can be 
 non-compliant with a compliant toolchain. The impact of a 
 certificate on your own processes is simply that tool 
 qualification has already happened elsewhere.


Correct. Safety and security are not really related. And even 
under the word safety there are different kinds of safety. For 
example the definition of a safe state is very different in 
different environments. For example in the nuclear sector some 
doors must *open* on failure while in some other sector they must 
*close*.

Also in the mobile sector (I've worked as a control systems 
developer for harvester heads) the definition of a safe state can 
be both to freeze all valves etc, but also to release all energy 
of the system depending on various factors (PLD cat3 iirc in that 
case).

So it's a complex topic that's for sure 😁

Today I work as a systems architect on a radio remote control 
company and safety is (unsurprisingly) important ofc.

I'm not really sure we need a certified compiler (although we 
currently have one for certain products). We have a dialog w most 
certification "institutions" and tbh some times I'd say we know 
better then they do what is really safe (depends ofc). There are 
also other techniques like black channel/box etc etc but that's 
another topic.

I'm writing on the phone atm, I can elaborate on what our 
requirements would be later. But one reason I looked into D in 
the first place was actually  safe and the things Walter talked 
about.

I have hope for D being useful for us.
Feb 09 2021
parent reply Max Haughton <maxhaton gmail.com> writes:
On Tuesday, 9 February 2021 at 19:59:02 UTC, Imperatorn wrote:

 On Tuesday, 9 February 2021 at 16:58:35 UTC, Gregor Mückl wrote:

 [...]


 Correct. Safety and security are not really related. And even 
 under the word safety there are different kinds of safety. For 
 example the definition of a safe state is very different in 
 different environments. For example in the nuclear sector some 
 doors must *open* on failure while in some other sector they 
 must *close*.

 [...]


I would like to write a bounded model checker for D although I 
make no guarantees because it's one more mad idea for the list of 
many mad ideas I have.
Feb 09 2021
next sibling parent reply lagfra <me fragal.eu> writes:
On Tuesday, 9 February 2021 at 21:23:35 UTC, Max Haughton wrote:

 I would like to write a bounded model checker for D although I 
 make no guarantees because it's one more mad idea for the list 
 of many mad ideas I have.


I have been considering the feasibility of implementing a model 
checker in D,
but a symbolic one, mainly because of the convenience of having 
straightforward
control over the GC. I've built some tiny bits (an extremely basic
implementation of decision diagrams and a parser for Büchi 
automata used in LTL
model checking).

It's a big project but IMHO it would be useful, if nothing else 
as a
benchmarking tool with respect to other model checkers written in 
different
languages (Java, C++) or different implementation choices (gc, 
nogc).
Feb 09 2021
next sibling parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Tuesday, 9 February 2021 at 23:59:32 UTC, lagfra wrote:

 On Tuesday, 9 February 2021 at 21:23:35 UTC, Max Haughton wrote:

 I would like to write a bounded model checker for D although I 
 make no guarantees because it's one more mad idea for the list 
 of many mad ideas I have.


 I have been considering the feasibility of implementing a model 
 checker in D,
 but a symbolic one, mainly because of the convenience of having 
 straightforward
 control over the GC. I've built some tiny bits (an extremely 
 basic
 implementation of decision diagrams and a parser for Büchi 
 automata used in LTL
 model checking).

 It's a big project but IMHO it would be useful, if nothing else 
 as a
 benchmarking tool with respect to other model checkers written 
 in different
 languages (Java, C++) or different implementation choices (gc, 
 nogc).


That sounds like a cool project
Feb 09 2021
prev sibling parent reply welkam <wwwelkam gmail.com> writes:
A talk about model checker Alloy. Its an introductory talk to 
people with not prior knowledge
"Finding bugs without running or even looking at code" by Jay 
Parlar
https://www.youtube.com/watch?v=FvNRlE4E9QQ
Feb 10 2021
next sibling parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Wednesday, 10 February 2021 at 17:01:19 UTC, welkam wrote:

 A talk about model checker Alloy. Its an introductory talk to 
 people with not prior knowledge
 "Finding bugs without running or even looking at code" by Jay 
 Parlar
 https://www.youtube.com/watch?v=FvNRlE4E9QQ


Nice. I've used UPPAAL in the past with some success.

https://en.wikipedia.org/wiki/Uppaal_Model_Checker
Feb 10 2021
prev sibling parent lagfra <me fragal.eu> writes:
On Wednesday, 10 February 2021 at 17:01:19 UTC, welkam wrote:

 A talk about model checker Alloy. Its an introductory talk to 
 people with not prior knowledge
 "Finding bugs without running or even looking at code" by Jay 
 Parlar
 https://www.youtube.com/watch?v=FvNRlE4E9QQ


That's actually an interesting SAT-based mc, though I never had 
the occasion of trying it out. I like the fact that it is 
currenly under development, in my experience model checkers are 
"old" (most theoretical breaktroughs have been published in the 
1980s and still struggle to get a proper implementation). Plus, 
research is mostly supported by universities, which implies that 
development pace is often quite slow.

A model checker that has been widely adopted is NuSMV 
(https://nusmv.fbk.eu/), there's a very nice survey by K. Rozier 
from NASA Ames research center describing an example application 
of it 
https://www.researchgate.net/publication/222531608_Linear_Temporal_Logic_Symbolic_Model_Checking
Feb 11 2021
prev sibling parent lagfra <me fragal.eu> writes:
 I would like to write a bounded model checker for D although I make no
 guarantees because it's one more mad idea for the list of many mad ideas I
 have.


I have been considering the feasibility of implementing a model checker in D,
but a symbolic one, mainly because of the convenience of having straightforward
control over the GC. I've built some tiny bits (an extremely basic
implementation of decision diagrams and a parser for Bchi automata used in LTL
model checking).

It's a long project but IMHO it would be useful, if nothing else as a
benchmarking tool with respect to other model checkers written in different
languages (Java, C++) or different implementation choices (gc, nogc).
Feb 09 2021
prev sibling parent Dukc <ajieskola gmail.com> writes:
On Tuesday, 9 February 2021 at 14:14:42 UTC, Bastiaan Veelo wrote:

 This makes me wonder what certifying the tool practically 
 brings to the table, apart from doors that can be entered with 
 a certificate only. If certification of the tool does not 
 improve the safety of the product and does not make it easier 
 to test the safety of the product, I have the feeling that the 
 certificate only improves perceived safety.


I quess the point is that at least the knowledge of the bugs the 
compiler has does not get old. If you always use the newest 
version of GCC for instance, there is the possibility that code 
changes due to new features or refactoring have caused new bugs 
since the bug manifestation site was last tested.

Still, one would think it'd be more efficient to certify a 
version of an open-source compiler from a public interest fund, 
and anyone could then use that version for free.
Feb 09 2021
prev sibling next sibling parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Tuesday, 9 February 2021 at 10:10:05 UTC, IGotD- wrote:

 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?


 Just to put it into some perspective. I have worked with so 
 called certified C/C++ compilers in the automotive industry. I 
 remember encountered several bugs in those compilers as well 
 they are usually far behind when adopting the new language 
 standards. Compare this to GCC, when was the last time you 
 encountered a bug in that compiler? I can't remember any.

 The certified compilers which are not better than GCC are 
 usually proprietary and cost money for each user. Here we have 
 a product that is essentially worse than GCC and cost money. 
 What it is really about is a form of corruption. The only 
 positive side is that if you find a bug you can put pressure on 
 the company that provides the compiler but usually that takes 
 several months.


There is a fair amount of hate in this post that I can't agree 
with. I've worked with certified compilers, too. It was mainly 
one of the major products in the field. The package was a mixed 
bag. The custom IDE is lacking and the proprietary build tools 
are not very good, but the actual compiler for our target 
platform turned out to be very good. We threw it at a pretty big 
preexisting codebase and it worked (we had a few places where we 
were relying on subtle UB - that's on us). Compared to GCC, the 
generated code would consistently be smaller and thus faster, 
even when I compared unoptimized builds to GCC with optimizations 
(curiously, speed optimized GCC output was smaller than size 
optimized output!).
Feb 09 2021
next sibling parent reply Max Haughton <maxhaton gmail.com> writes:
On Tuesday, 9 February 2021 at 13:35:36 UTC, Gregor Mückl wrote:

 On Tuesday, 9 February 2021 at 10:10:05 UTC, IGotD- wrote:

 [...]


 There is a fair amount of hate in this post that I can't agree 
 with. I've worked with certified compilers, too. It was mainly 
 one of the major products in the field. The package was a mixed 
 bag. The custom IDE is lacking and the proprietary build tools 
 are not very good, but the actual compiler for our target 
 platform turned out to be very good. We threw it at a pretty 
 big preexisting codebase and it worked (we had a few places 
 where we were relying on subtle UB - that's on us). Compared to 
 GCC, the generated code would consistently be smaller and thus 
 faster, even when I compared unoptimized builds to GCC with 
 optimizations (curiously, speed optimized GCC output was 
 smaller than size optimized output!).


What architecture was this running on? I say that because small 
is often not fast on a big machine - and the reason why fast gave 
smaller code is probably because of the weird non-determinism you 
get in big compilers as more stuff is inlined giving way to more 
information for the optimizer to use locally.
Feb 09 2021
parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Tuesday, 9 February 2021 at 13:42:51 UTC, Max Haughton wrote:

 On Tuesday, 9 February 2021 at 13:35:36 UTC, Gregor Mückl wrote:

 On Tuesday, 9 February 2021 at 10:10:05 UTC, IGotD- wrote:

 [...]


 [...]


 What architecture was this running on? I say that because small 
 is often not fast on a big machine - and the reason why fast 
 gave smaller code is probably because of the weird 
 non-determinism you get in big compilers as more stuff is 
 inlined giving way to more information for the optimizer to use 
 locally.


The specific project that allowed me to make that comparison had 
an ultra low power Cortex-M4. That's an in-order design with 3 
pipeline stages and no optimizations for branching. So it's 
primitive enough that raw instruction count translates directly 
into performance.
Feb 09 2021
parent Max Haughton <maxhaton gmail.com> writes:
On Tuesday, 9 February 2021 at 17:25:17 UTC, Gregor Mückl wrote:

 On Tuesday, 9 February 2021 at 13:42:51 UTC, Max Haughton wrote:

 On Tuesday, 9 February 2021 at 13:35:36 UTC, Gregor Mückl 
 wrote:

 [...]


 What architecture was this running on? I say that because 
 small is often not fast on a big machine - and the reason why 
 fast gave smaller code is probably because of the weird 
 non-determinism you get in big compilers as more stuff is 
 inlined giving way to more information for the optimizer to 
 use locally.


 The specific project that allowed me to make that comparison 
 had an ultra low power Cortex-M4. That's an in-order design 
 with 3 pipeline stages and no optimizations for branching. So 
 it's primitive enough that raw instruction count translates 
 directly into performance.


I'm slightly surprised GCC generated larger code, but I can see 
it happening for something of that size.
Feb 09 2021
prev sibling parent reply IGotD- <nise nise.com> writes:
On Tuesday, 9 February 2021 at 13:35:36 UTC, Gregor Mückl wrote:

 There is a fair amount of hate in this post that I can't agree 
 with.


Then you have a crewed up idea what hate means. Hate does not 
mean that you disagree with someone.


 I've worked with certified compilers, too. It was mainly one of 
 the major products in the field. The package was a mixed bag. 
 The custom IDE is lacking and the proprietary build tools are 
 not very good, but the actual compiler for our target platform 
 turned out to be very good. We threw it at a pretty big 
 preexisting codebase and it worked (we had a few places where 
 we were relying on subtle UB - that's on us). Compared to GCC, 
 the generated code would consistently be smaller and thus 
 faster, even when I compared unoptimized builds to GCC with 
 optimizations (curiously, speed optimized GCC output was 
 smaller than size optimized output!).


The main reason some company uses a certain "certified" compiler 
is because the customer demands it. There in between anything is 
possible with any kind of back room deal. Just like doctors get 
money under the table in order to promote a certain drug, which 
we know is commonplace.

The compiler I have worked with had a number of bugs and then I 
tried GCC and of course it ran perfectly with better code 
generation. The answer is of course obvious GCC is used by the 
hundreds of thousands and many contributing to the compiler. This 
compared to a small company creating some "certified" compiler. 
I'm all of commercial SW but I cannot deny that the huge backing 
of the GCC compilers is hard to beat. If I would decide which 
compiler to use I would of course go with GCC and skip the 
certified compiler, however it is the customers that dictates 
what to use.
Feb 09 2021
parent Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Tuesday, 9 February 2021 at 14:54:35 UTC, IGotD- wrote:

 On Tuesday, 9 February 2021 at 13:35:36 UTC, Gregor Mückl wrote:

 There is a fair amount of hate in this post that I can't agree 
 with.


 Then you have a crewed up idea what hate means. Hate does not 
 mean that you disagree with someone.


Please allow me to retract the part mentioning hate. That may 
have gone too far. I'm sorry if I offended you.


 I've worked with certified compilers, too. It was mainly one 
 of the major products in the field. The package was a mixed 
 bag. The custom IDE is lacking and the proprietary build tools 
 are not very good, but the actual compiler for our target 
 platform turned out to be very good. We threw it at a pretty 
 big preexisting codebase and it worked (we had a few places 
 where we were relying on subtle UB - that's on us). Compared 
 to GCC, the generated code would consistently be smaller and 
 thus faster, even when I compared unoptimized builds to GCC 
 with optimizations (curiously, speed optimized GCC output was 
 smaller than size optimized output!).


 The main reason some company uses a certain "certified" 
 compiler is because the customer demands it. There in between 
 anything is possible with any kind of back room deal. Just like 
 doctors get money under the table in order to promote a certain 
 drug, which we know is commonplace.


This is not representative of all industries everywhere. My own 
personal experience showed  me that there are places where this 
is taken seriously for good reasons. It seems that you and I have 
made very different experiences during our careers. Nothing wrong 
with that, I guess.


 The compiler I have worked with had a number of bugs and then I 
 tried GCC and of course it ran perfectly with better code 
 generation. The answer is of course obvious GCC is used by the 
 hundreds of thousands and many contributing to the compiler. 
 This compared to a small company creating some "certified" 
 compiler. I'm all of commercial SW but I cannot deny that the 
 huge backing of the GCC compilers is hard to beat. If I would 
 decide which compiler to use I would of course go with GCC and 
 skip the certified compiler, however it is the customers that 
 dictates what to use.


In my experience, the quality of GCC code generation varies a lot 
depending on the target platform. It's an extremely good compiler 
for desktop/server class CPUs, but in my experience, it doesn't 
target small embedded platforms very well. This low end seems to 
be too niche to attract many developers to GCC or LLVM.
Feb 09 2021
prev sibling parent Elronnd <elronnd elronnd.net> writes:
On Tuesday, 9 February 2021 at 10:10:05 UTC, IGotD- wrote:

 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 2. Are there any plans to make a certified compiler?


 Just to put it into some perspective. I have worked with so 
 called certified C/C++ compilers in the automotive industry. I 
 remember encountered several bugs in those compilers as well 
 they are usually far behind when adopting the new language 
 standards. Compare this to GCC, when was the last time you 
 encountered a bug in that compiler? I can't remember any.


You may mean different things by ‘certified’.

In some contexts, the term refers to a formally verified 
compiler, like, cakeml or compcert, which has been mathematically 
proven not to have any compilation bugs.  I would be inclined to 
trust such a compiler.
Mar 17 2021
prev sibling next sibling parent Dukc <ajieskola gmail.com> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?


One would presumably certify some version of the D compiler, 
let's say 2.095.0, and would have to use that for years to come. 
Perhaps patch version updates would be okay (2.095.1), but no 
updating to 2.096.0 without re-certifying.

My experience is that Dub projects tend to stop compiling after 
perhaps 5 or so versions on average. That means that if D 
libraries are used, one would have to start maintaining them 
themselves after some time. This isn't a showstopper, since such 
maintenance is not a major burden assuming the library is already 
stable and no new features are desired. But it means that if 
someone releases a D library 3 years after the certification, the 
new library probably can't be used without considerable porting 
effort. One would be fairly much stuck with what exists at 
certification time.
Feb 09 2021
prev sibling parent reply Arun <aruncxy gmail.com> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?


If C is ready for safety critical applications, then DasBetterC 
is beyond ready. HN discussions on the related topic here: 
https://news.ycombinator.com/item?id=23005297
Feb 17 2021
parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Wednesday, 17 February 2021 at 17:36:41 UTC, Arun wrote:

 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:

 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?


 If C is ready for safety critical applications, then DasBetterC 
 is beyond ready. HN discussions on the related topic here: 
 https://news.ycombinator.com/item?id=23005297


Nice, i guess they were more thinking of GDC, idk. I can ask 
again.

 everyone:
Btw, where can I download gcc with D support and what version of 
D is it?

I've heard rumors it will be updated "soon", is that correct? 🤔

Thanks!
Feb 19 2021