[f00_]

The most interesting thing I've seen as far as this is concerned is Taint Analysis. You can label functions as returning user input, some functions take user input and turn it into sanitized input, and there are functions that should never take non-sanitized input.

It's all statically-checked and you can incorporate it into your CI/CD: https://pyre-check.org/docs/pysa-basics.html

See also: Property-based testing, and TLA+

[sk5t]

FWIW the first practical application of input tainting that comes to mind is Perl's circa 2001, although I wouldn't be surprised to hear Smalltalk went there before.

[eesmith]

FWIW, perl3 circa 1990 - https://en.wikipedia.org/wiki/Taint_checking#History .

[rurban]

Yeah, but with holes. Eg affecting Bugzilla. Only closed 2018 in cperl (hash keys). perl5 never cared to close its taint holes.

[bawolff]

I'm not familar with pyre, but i have experimented with some security static analysis tools. The one's i have experimented with take some normal program and try to analyse it. The analysis is usually far from complete, and as a result has so many false positives that its difficult to adopt.

Anyways, i would say those are rather different from systems where you give an actual proof of correctness.