D for safety critical applications

[Imperatorn]

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