3 ms·

I was doing ASIC design and verification for 5 years before I switched to software and I think it led me to write much higher quality code and tests. I was used

I was doing ASIC design and verification for 5 years before I switched to software and I think it led me to write much higher quality code and tests. I was used to making 100% sure everything was correct, because fixing bugs in silicon is extremely difficult and expensive. You are also forced to spend more time defining architecture and interfaces ahead of time, which can be very useful/important for certain software projects. Integration tests usually seem to find the most important bugs, but on hardware they take hours or days to run. With that limitation removed in software development, they're almost too good to be true. I'd also be interested in seeing how formal verification could be applied to software development.

exdsq 5y ago
Formal verification is used in software development! Check out Coq, Lean, Agda, Lean, TLA+, or any links when you google those tools :)
- fouric 5y ago
  Lean: so good, we mentioned it twice. I've heard that ACL2 is also a thing that exists. To me, one of the most intimidating parts of getting into formal verification is deciding which system to use - as you mentioned, there are several. What are the strengths and weaknesses of each?
  - exdsq 5y ago
    Hahahaha good catch. Perhaps if I'd used Lean on that string it wouldn't have happened. I think the big choice is between using lightweight or heavy tools. Things like Coq and Agda take a lot of time to learn and implement but can derive 'correctly Haskell code which you can use, while TLA+ is more like a blueprint tool to check an algorithm before you write it in {favourite_language}. I think it's practical to learn TLA+ but if it's purely for intellectual satisfaction Wadler has a good book called Programming Foundations in Agda (I think?) which is available for free online.
namibj 5y ago
They did do formal verification for a microkernel: https://sel4.systems https://sel4.systems It's afaik the most complex piece of software with full formal verification to date.
bradleyjg 5y ago
There’s some software projects that look a lot like hardware and would benefit from crossover learnings. There’s also lots of software projects where the hard part is not building out the code but instead figuring out what to build. A lot of the differences in common practices are due to that, not because software developers are foolish or lazy. To give concrete examples: Intel knows what it needs to accomplish in order to win back the top spot. There are tons of challenges to get there, but the end goal is clear. That’s an entirely different kind of problem from Twitter needing to figure how to monitize.

exdsq 5y ago

Formal verification is used in software development! Check out Coq, Lean, Agda, Lean, TLA+, or any links when you google those tools :)

fouric 5y ago
Lean: so good, we mentioned it twice. I've heard that ACL2 is also a thing that exists. To me, one of the most intimidating parts of getting into formal verification is deciding which system to use - as you mentioned, there are several. What are the strengths and weaknesses of each?
- exdsq 5y ago
  Hahahaha good catch. Perhaps if I'd used Lean on that string it wouldn't have happened. I think the big choice is between using lightweight or heavy tools. Things like Coq and Agda take a lot of time to learn and implement but can derive 'correctly Haskell code which you can use, while TLA+ is more like a blueprint tool to check an algorithm before you write it in {favourite_language}. I think it's practical to learn TLA+ but if it's purely for intellectual satisfaction Wadler has a good book called Programming Foundations in Agda (I think?) which is available for free online.

namibj 5y ago

They did do formal verification for a microkernel: https://sel4.systems https://sel4.systems It's afaik the most complex piece of software with full formal verification to date.

bradleyjg 5y ago

There’s some software projects that look a lot like hardware and would benefit from crossover learnings. There’s also lots of software projects where the hard part is not building out the code but instead figuring out what to build. A lot of the differences in common practices are due to that, not because software developers are foolish or lazy. To give concrete examples: Intel knows what it needs to accomplish in order to win back the top spot. There are tons of challenges to get there, but the end goal is clear. That’s an entirely different kind of problem from Twitter needing to figure how to monitize.