[Hol-info] hardware verification

[Gergely B. <gb...@gm...>]

Hi,

my question is not strictly about the HOL family of provers but since
the most successful application area for HOL is hardware verification
I think this is the right place to ask.

There is a research on functional, i.e. purely functional description
languages: CλaSH. reFLect, Lava, Confluence, HDCaml, Bluespec, SAFL
etc.

http://www.hindawi.com/journals/isrn/2012/271836/ wrote in 2012 that

"There are only few published circuit designs developped using FHLs"

Is this because the functional description languages are not mature
yet, or simply the hardware industry does not want to move from the
used and proven methods of VHDL, Verilog and SystemC, despite of their
verbosity? Also there can be a resistance of engineers to learn a
non-C-like language?

- Gergely