D for safety critical applications

[lagfra]

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).