[gaudat]

I miss this kind of stuff in computer programming languages.

In hardware design, verification is done simultaneously with design, and semiconductor companies would be bankrupt if they did not verify the hell out of their designs before committing millions in manufacturing these chips.

Even among hobbyists this is getting traction with yosys.perhaps its time for programmers to adapt this kind of tooling so there will be less buggy software released...

[vacuity]

There are probably orders of magnitude in difference between hardware design output and programming output. At least at the time, seL4's verification was quite impressive for a codebase on the order of 10,000 lines. But we should work towards the goal of improved formal modelling and checking all the same.