Hacker Timesnew | past | comments | ask | show | jobs | submitlogin

> its written in F#, so you have to trust your CLI implementation to be bug-free as well

Is that any different to an implementation in C relying on the processor being bug-free?



If you count up all of the possible states a processor can be in, as well as the number of transitions between them, you'll come up with a very big number of possible execution paths you'll need to verify work correctly. However, if you do the same for the CLI (or any non-trivial piece of software), you'll come up with a much, much, MUCH bigger number. As in, each additional state the CLI can enter potentially doubles the number of possible execution paths you'll need to check.

The number of states and transitions for a processor today is large, but not so large that engineers can't formally and automatically verify that the processor will behave correctly under all inputs. Also, the structure of the processor and the way it is specified (i.e. Verilog) make it amenable to formal verification.

This is not true for most software, not even things written in Haskell. You can cover a lot of cases with automated software testing, but you'll find that it's very, very, VERY hard to prove that you've covered every possible case. Even if you can, modeling multiple instances of the system as they evolve in time (i.e. any networked system or interactive system) means you have to consider all possible combinations of states they can be in.

To put into perspective how hard formal verification of software is, I have a story. A friend of mine did his masters thesis on modifying TCP to allow for host mobility, and formally proving the correctness of his new TCP protocol. Despite having a 100-node cluster of beefy (48GB RAM) compute nodes at his disposal, it simply didn't have enough total RAM to verify the correctness of his protocol beyond five rounds of communication between one client and one server.

Unless the CLI developers add machine-checked but hand-crafted proofs of correctness for each and every method, I trust the processor to be bug-free far more than any piece of software it runs. Now of course, if the NSA tampers with either, then all bets are off :P


The CLI is running in a processor, isn't it? I guess your argument is that the software using CLI is potentially affected by more bugs ;)




Consider applying for YC's Summer 2026 batch! Applications are open till May 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: