[IsTom]

A lot of software doing useful work halts pretty trivialy, consuming inputs and doing bounded computation on each of them. You're not going to recurse much in click handlers or keep making larger requests to handle the current one.

[spr-alex]

I was just very naive at 18 about program analysis. I haven't lost my imagination though. I was a self-taught IOI gold division competitor. I thought every problem had an algorithm. It doesn't work like that. Program analysis is collecting special snowflakes that melt in your hand. There is no end to the ways you can write a bug in C. Ghosts of Semmle, Semgrep, Coccinelle past, be humbled. LLMs saturate test coverage in a way no sane human would. I do not think they can catch all bugs because of the state space explosion though, but they will help all programmers get better testing. At the end of the day I believe language choice can obviate security bugs, and C/C++ is not easy or simple to secure.

[nickpsecurity]

You've never seen the full power of static analysis, dynamic analysis, and test generation. The best examples were always silo'd, academic codebases. If they were combined, and matured, the results would be amazing. I wanted to do that back when I was in INFOSEC.

That doesn't even account for lightweight, formal methods. SPARK Ada, Jahob verification system with its many solvers, Design ny Contract, LLM's spitting this stuff out from human descriptions, type systems like Rust's, etc. Speed run (AI) producing those with unsafe stuff checked by the combo of tools I already described.

[saagarjha]

Silo’d, academic codebases are not under the kind of attacks that commodity software is

[nickpsecurity]

The silo'd codebases I was referring to are verification tools they produce. They're used to prevent attacks. Each tool has one or more capabilities others lack. If combined, they'd catch many problems.

Examples: KLEE test generator; combinatorial or path-bases testing; CPAChecker; race detectors for concurrency; SIF information flow control; symbolic execution; Why3 verifier which commercial tools already build on.

[saagarjha]

"Each lacks capabilities" is not a strong sell for "together they can catch most problems".

[IsTom]

If you start with safety in mind and don't just try to bolt it on, you're in a much better place. With the kind of code you need in typical applications you could force vast majority of it in a shape that passes termination checks in theorem provers without much overhead, especially if you can just put gnarly things in standard libarary and validate (with proofs hopefully) once.

Though starting with C/C++ is a losing proposition in that regard. And I guess any kind of discipline loses to just throwing half-baked javascript at wall, because deadlines don't care about bugs.