Re: [Hol-info] hardware verification and dependent types

[Ken K. <ma...@ke...>]

Most hardware verification seems to be done in some variant of HOL, and its type system is too poor for dependent type theory (and even for type abstraction).
Freek Wiedijk: "The HOL type system is too poor. As we already argued in the previous section, it is too weak to properly do abstract algebra." [Wiedijk, 2007, p. 130]
	http://www.owlofminerva.net/files/fom.pdf#page=10
See also:
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-September/msg00045.html
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-April/msg00102.html

Tom Melham's Extended HOL provides quantification over types, but no type abstraction and no dependent types.
HOL2P and HOL-Omega do have type abstraction, but do not provide full dependent types (if I'm not mistaken):
	http://www.owlofminerva.net/files/fom.pdf#page=1

For full dependent type theory substitution at the type level is required.
I had implemented this at some stage in the development of R0, but removed it later since it seemed too experimental then:
	"[O]ne would like to infer from fuv(2):vectype(2) to fuv(2):R^2. An implementation of a substitution rule directly at the type (subscript) level appeared too experimental to the author and was removed, since further case studies (here using the recursion operator R) should be undertaken."
	http://www.owlofminerva.net/files/formulae.pdf#page=12
Plus, the efforts for formalizing the proofs in a Hilbert-style system for the recursion operator R necessary for number theory were too large:
	"As shown further below [pp. 388 ff.], the recursion operator R [Andrews, 2002, pp. 281 f., 284] can be used to define a function which obtains the type of a vector of a given dimension."
	http://www.owlofminerva.net/files/formulae.pdf#page=12

One option might be implementing a natural deduction variant of R0 (with substitution at the type level) in a logical framework such as Isabelle or Metamath.
Cris Perdue has implemented a natural deduction variant of Q0:
	http://prooftoys.org
	http://mathtoys.org
	http://www.owlofminerva.net/files/fom.pdf#page=2
Since Q0 and R0 use the description operator, one would also get rid of the epsilon operator in HOL and the implicit Axiom of Choice (the use of which then, as desired, would become explicit).
Mike Gordon: "It must be admitted that the ε-operator looks rather suspicious." [Gordon, 2001, p. 24] "The inclusion of ε-terms into HOL 'builds in' the Axiom of Choice [...]." [Gordon, 2001, p. 24]
	http://www.owlofminerva.net/files/fom.pdf#page=9


Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota
http://doi.org/10.4444/100



> Am 30.04.2019 um 15:28 schrieb Lawrence Paulson <lp...@ca...>:
> 
> In hardware, most devices are parameterised by a numerical bit width: buses, counters, adders, registers, etc. So it seems obvious that people might have tried to perform hardware verification using some form of dependent type theory. Are there any particularly notable achievements along those lines? And if not, why not?
> 
> Larry Paulson