I do agree with point 1 and with most of point 2 besides some more arcane things like intentionally racy memory access and some write-cache eviction instruction

I do agree with point 1 and with most of point 2 besides some more arcane things like intentionally racy memory access and some write-cache eviction instruction not being properly modeled (in for example Rust).