You don't have to believe me either; if you try it, you should generally see that they have the same performance.

Here are some fairly realistic examples.

1. Rust : http://benchmarksgame.alioth.debian.org/u64q/compare.php?lan...

2. Swift : http://benchmarksgame.alioth.debian.org/u64q/compare.php?lan...

As for a SAT solver, I was not speaking out of my ass. Here is one try that got a fair bit of attention. https://github.com/mishun/minisat-rust

Yeah, we've had some small regressions recently; a few months ago we were usually faster, now we're slightly slower. Still generally close, except for the ones that need explicit SIMD, as that's still being designed.

When you say "naive SAT solver" do you mean one where you hard-code a boolean formula with N variables and then check every possible solution (from 0 to 2^N)? If so, does this kind of program accurately characterize the kind of work a kernel does?

No, something like the CDCL algorithm without domain specific heuristics and tweaks. I expect that is fairly representative in terms of ..say.. common data structures needed in most systems.