[johnbender]

To follow on this sentiment at a slight tangent, I am happy for the enthusiastic attempts from all quarters but folks seem to misunderstand that incremental progress in academia is often due to the problems being very hard. Formal verification in the presence of weak memory models is an ongoing problem that only recently has seemed tractable thanks to the hard work of the folks at MPI etc over more than a decade of publications and iterating on logics like Iris