This page lists all soundness-related flaws found since HOL Zero version 0.3.0 (released 2010-09-14), together with any successful bounty claims. All list entries would qualify for a bounty reward. The list consists of any logical unsoundnesses (i.e. in the design or implementation of the logic), and those printer unsoundnesses that can be exploited to make it appear that there is a logical unsoundness.
Problem: Printer unsoundness. The display of some UTF-8 characters could, under certain circumstances, look identical to the display of other characters, thus potentially resulting in misleadingly-displayed theorems. HOL Zero 0.3.0.
Action taken: More careful implementation of character escaping for non-ASCII-printable characters. HOL Zero 0.3.1.
Claimant: Martin von Gagern awarded $100
Problem: Logical unsoundness. OCaml's 'Obj.magic' function could be used to type-convert an arbitrary sequent into a theorem. HOL Zero 0.3.0.
Action taken: Circumventing ML type system added to list of banned practices. HOL Zero 0.3.1.
Claimant: Carl Witty awarded $100
Problem: Printer unsoundness. OCaml string mutability could be exploited to alter the fixity of an identifier without notifying the user, thus potentially resulting in misleadingly-displayed theorems. HOL Zero 0.4.2.
Action taken: Protection against exploiting string mutability added to fixity commands. HOL Zero 0.4.3.
Claimant: None
Problem: Printer unsoundness. The pretty printer did not put parentheses around let-expressions when they occurred as subexpressions, thus potentially resulting in misleadingly-displayed theorems. HOL Zero 0.4.3.
Action taken: Pretty printer adjusted to add parentheses for let-expression subexpressions. HOL Zero 0.4.4.
Claimant: None
Problem: Printer unsoundness. The lexical status of the string used for turnstile ("|-") was not a reserved word, thus potentially resulting in misleadingly-displayed theorems. HOL Zero 0.4.4.
Action taken: Turnstile now made a reserved word. HOL Zero 0.4.5.
Claimant: None
Problem: Printer unsoundness. The preterm destructors for let-expressions, enumeration expressions and compound infix expressions did not correctly destruct subterms involving variables overloaded with the top-level constant/variable, thus potentially resulting in misleadingly-displayed theorems. HOL Zero 0.4.6.
Action taken: Preterm destructors corrected. HOL Zero 0.4.7.
Claimant: None
Problem: Printer unsoundness. OCaml string mutability could be exploited to alter the enumeration brackets associated with a given enumeration insertion operator and empty structure constant, without notifying the user, thus potentially resulting in misleadingly-displayed theorems. HOL Zero 0.5.0.
Action taken: Protection against exploiting string mutability added to enumeration bracket commands. HOL Zero 0.5.1.
Claimant: None