[rtpg]

There are plenty of projects pushing the state of the art forward.

A very specific example: basically all interactive theorem proving tooling is built in public research halls. This has allowed Compcert, a C compiler with “no bugs”[0] to exist.

The Compcert case is interesting because private funding is also involved. Public state research can still pull in private funds! We are not entirely throwing in the towel!

[0] “no bugs” here means “we have defined a spec for C, and this compiler is guaranteed to compile your C code along the spec we defined, so long as your program terminates”. There’s some hand waving around a theorem prover’s own validity but all Compcert bugs have been “we misewrote a chunk of spec” varietals