Probably rather alien to the HN crowd ;)
The only fully automated lines are 1 and 14.
First real success was Meteor line 14 driverless metro in Paris: Over 110 000 lines of B models were written, generating 86 000 lines of Ada. No bugs were detected after the proofs, neither at the functional validation, at the integration validation, at on-site test, nor since the metro lines operate (October 1998). The safety-critical software is still in version 1.0 in year 2007, without any bug detected so far.
From: http://rodin.cs.ncl.ac.uk/Publications/fm_sc_rs_v2.pdf
|bool foo(bool i, bool j) {
2| return i ||
1| j;
|}
|
|void main() {
1| foo(true, false);
1| foo(false, false);
|}