[libre-riscv-dev] [Bug 207] Design Rust-based HDL like nmigen (deferred for later)

bugzilla-daemon at libre-riscv.org bugzilla-daemon at libre-riscv.org
Wed Mar 4 03:23:05 GMT 2020


--- Comment #4 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Samuel Falvo II from email)
> I can see the benefit that algebraic types can offer; however, it's not
> clear to me how Rust's borrow-checker would be a benefit for synthesis, or
> logic design at all for that matter.  Have you run into a situation in the
> past where the borrow checker would have proven advantageous to have around?

I was thinking lifetimes might be useful for proving that combinatorial logic
doesn't have loops.

Most of the benefit I can see is not actually the algebraic sum (enum/union)
types, but actually Rust's generics, trait system, compile-time function
evaluation (const fn -- like C++ constexpr), and const-generics (generics based
on values rather than types).

> (In reply to Jacob Lifshay from comment #3)
> > (In reply to Luke Kenneth Casson Leighton from comment #2)
> > > if there was ever a compelling reason to do this it would be if there was,
> > > like BSV, a 100% guarantee that syntactically-correct HDL was
> > > synthesiseable.  this however is only the case in BSV because it utilises
> > > the formal proof / functional programming aspects of Haskell.
> > 
> > Rust does support type and lifetime-based formal proofs, which is one of the
> > reasons I really like it.

You are receiving this mail because:
You are on the CC list for the bug.

More information about the libre-riscv-dev mailing list