Fearmonger is a little heavy handed but the comparison to Dwarf Fortress is probably too strong.
I don't find F* syntax anymore intimidating than Haskell, Scala, Mercury, Prolog, etc. aka the hard languages. I love Ruby and I didn't find it intuitive when I first began learning it (specifically, the block/lambda passing mechanism).
Meanwhile I'm sure there's people out there baffled that anyone finds dwarf fortress challenging to get into.
I'm old enough that I've had the pleasure of handholding software engineers through their first anonymous function usage. Effect system, refinement types, totality checker? The best I get is blank stares before they go back to C# and JavaScript. These days I'm just glad they tolerate linq expressions and typescript.
It matters where you're standing for what feels incomprehensible. But then again, you can say the same thing about dwarf fortress.
How does this relate to the topic? I'm willing to assume it does, I just don't get it. I'm probably overreacting because when Scott was writing this, tens of thousands of Scots living in poverty were being evicted via arson from their land and country. Saying they were dead in spirit is very elitist as he sat in comfort.
Also
> if you've worked with other proof oriented languages.
That's doing a lot of heavy lifting.