Author here. "Now what have we bought ourselves? Not much." Well of course I disagree with that statement. My work on Metron suggests that we've bought oursel

Author here. "Now what have we bought ourselves? Not much." Well of course I disagree with that statement. My work on Metron suggests that we've bought ourselves a way to write programs that can execute on both CPUs and FPGAs, which is a valuable thing. The ability to more directly translate the behavior of our programs into a proof framework like TLA is also quite useful, and I think folks who are deep into functional programming also like the lack of "side effects" since the process of computing x' is guaranteed not to change x (or any other observable property of the previous program state).