ymherklotz

No I think it's fine. On another note, I have proven Fermat's Last Theorem with z3 using this setup :) and it goes faster if you reduce a variable called "timeout" for some reason!

  from z3 import *
  
  s = Solver()
  s.set("timeout", 600)
  a = Int('a')
  b = Int('b')
  c = Int('c')
  s.add(a > 0)
  s.add(b > 0)
  s.add(c > 0)
  theorem = a ** 3 + b ** 3 != c ** 3
  if s.check(Not(theorem)) == sat:
      print(f"Counterexample: {s.model()}")
  else:
      print("Theorem true")

I mean you could ship GNU info documentation (for which I saw a quick mention in the Blog post, but thought I’d mention why I like it). These can be generated from a variety of sources, including markdown. When installed alongside your app, they would show up in the top level heading when launching info, making it nicely discoverable if you use info.

As a bonus, this means the documentation will always be up to date with the version you are using. I guess if you want to look at older or newer versions the downside is you’ll have to download the app.

Clash compiles to Verilog or VHDL, just like most higher-level hardware description languages (Bluespec is another interesting one which has a Haskell-like dialect and the compiler is written in Haskell).

It's impractical for most new/independent hardware languages to go to some kind of netlist, because the components/modules you will have available will vary greatly depending on your final target. Depending on if you are going to target a specific Intel FPGA, Xilinx FPGA or even a custom ASIC with a specific cell library, the netlist will look very different, and even the tools translating from Verilog will look different.

As an aside though, Verilog is quite versatile, so you can actually represent a netlist in Verilog itself with custom cell libraries. Instead you refer to Verilog you normally write in as a register transfer level (RTL) description.

The benefit is uniformity, everythings the same, which is one of the main reasons I use Emacs. I can use all of my usual navigation keys to move around the documentation of the variable, evaluate things inline, etc.. Just as if it were more text, which is what Emacs is already great at. I would mind the buttons getting a more modern look, but I think everything being text what makes it works this seemlessly, and it would be much tougher to get a uniform feel with graphical windows.