February 09, 2021
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).
February 10, 2021
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
February 10, 2021
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
February 10, 2021
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

February 11, 2021
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
February 17, 2021
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
February 19, 2021
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!
March 17, 2021
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.
March 17, 2021
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
March 17, 2021
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.