D for safety critical applications

[lagfra]

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