Fine but cutting the thought process at "it depends" is not a great way to understand what's happening here. You can explain anything happening at any company by saying "they need certain things more than whatever else they could spend that time on".

Why is PBT useful at Jane Street, at least more than in other places? Is it the use of functional language? Average Jane Street dev being more familiar with PBT? Is the domain particularly suited to this style of testing?

Explicitly, my claim is that the biggest bottleneck is education on how to use PBT effectively and Jane Street is not using them to get an extra mile in safety, they use it because it's the easiest way to write large chunk of the tests.