|
|
|
|
|
|
by GregarianChild
127 days ago
|
|
|
This is wrong as the others replies also point out. Tactics in LCF-style provers are not part of the TCB. Here is an example of the TCB for an industrial strength prover: ○ https://github.com/jrh13/hol-light/blob/master/fusion.ml A mere 676 LoCs. This miniscule size of the TCB is where the comparatively lesser bug count (despite intense use) comes from. |
|
|