3 ms·

Ask HN: Would you pay to have code verified?

• eimrine 3y ago
  Who will verify your verification as valuable?
  • ak1930 3y ago
    Because of the early stage of our tool it would have to be the customer, like in consulting. Naturally, we will provide full formal proofs in as explicit detail as is desired, down to the axioms of the language we're working in.
    • eimrine 3y ago
      I am not your client type of guy but at least I am fond of PVS-studio. They have a blog on 2 languages with revealing a lot of problems their product solves. Also they actively scan a lot of open-source software.
• zer8k 3y ago
  Sort of a meta question: this is a well trodden path. Code verification is very popular with government types. Have you considered trying to figure out what they're using and what they're paying? I see this as the same problem starting a CA is. To get trust you need to build trust. It's a catch 22. Formal verification is not necessary for 99% of code. Of that small 1% of code bases you're talking about aerospace, government contract work, and medical technology. I wouldn't even know how to guess at a price because if you can beat them at their own game you can probably attach as many zeroes as you want to it. What do you do if your verification fails though? Any company worth their salt will sue you into the ground. Especially if it results in a shuttle turning into a lawn dart. One last thing: are you verifying code or compiler? Especially with compiled languages verifications would have to be pegged to a compiler version, distributor, and standard. There's a reason aerospace is about 20 years behind modern compilers and it's not bureaucracy.
  • ak1930 3y ago
    Very interesting thoughts. We're verifying code. The idea here is not to close massive contracts with govts or SpaceX, but work on far smaller projects—even potentially open source ones—where there is an interest in correctness.
• schoen 3y ago
  Are you thinking of offering to write the formal specifications too, or try to formally verify compliance to a customer's specification? Does your tool attempt to mechanically create its own proof that the specification is satisfied by the code, or does that involve human effort? (Or both?)
  • gregjor 3y ago
    Was going to ask the same question. Verify against what exactly?
  • ak1930 3y ago
    Yes, in this case we would work with you to write the specifications. It does involve effort; the tool does not derive this in an automated way.
    • schoen 3y ago
      I don't personally have a use for this or the ability to pay for it, but I think this is a very valuable service, at least if you can demonstrate that you can do it repeatably for different kinds of code bases and different kinds of specified behaviors. Obviously, given Rice's Theorem, you can't do it "repeatably" for any arbitrary problem that a customer gives you, or else you would have to be omniscient with respect to all of mathematics... but "can probably verify behaviors that are similar to those that have been able to be verified before, in code bases that are similar to those where behaviors have been formally proven in the past" is still good!
• nexnex123 3y ago
  [flagged]
• ilaksh 3y ago
  What exactly are you verifying? Would you verify something about Rust code? And what would you verify?
  • ak1930 3y ago
    We would work with you to make formal specifications and then verify that your code satisfies them, and help modify it until it does. We are open to Rust, yes.
• throwawayadvsec 3y ago
  so what's the difference with QA+pentesting+tdd? what do you verify?
  • trealira 3y ago
    I'm not OP, and my comment is 7 days late, but I'll answer. With formal verification, you make a specification, and then prove that your program adheres to the specification as written. This is usually done with a proof assistant to ensure the proof is sound. The sel4 microkernel is a good example. The kernel is written in C, but the specification and proofs are written in Isabelle, a proof assistant. Specification and proofs: https://github.com/seL4/l4v https://github.com/seL4/l4v The microkernel itself: https://github.com/seL4/seL4 https://github.com/seL4/seL4 The main practical difference between testing and formal verification is that testing alone cannot guarantee correctness, i.e., the absence of errors in a program; it can only reveal errors, with no guarantee of revealing all of them. The only way to prove correctness is to write a proof of adherence to a specification. I found a good example of this from an excerpt of the book Program Construction by Roland Backhouse. The code is in Pascal. The problem the students had been set was to write a program that would compare two strings for equality. One student's solution was to assign the value true or false to a boolean equal as follows: equal := (string1.length = string2.length) if equal then for i := 1 to string1.length do equal := (string1.character[i] = string2.character[i]) The problem with this code is that it returns the value true whenever the two strings have equal length and their last characters are identical. For example, the two strings 'cat' and 'mat' would be declared equal because they both have length three and end in 't'. The student was quite taken aback when I demonstrated the error. Indeed, upon further questioning, it emerged that the program had been tested quite systematically. First, it had been tested on several pairs of identical strings, and then on several pairs of strings of unequal length. Both these tests had produced satisfactory results. The final test had been to input several pairs of equal length but unequal strings, such as 'cat' and 'dog', or 'house' and 'river'. This final test is interesting because it is possible to use simple probability theory to make a rough estimate of the chances of discovering the programming error. The details are not relevant here. Suffice it to say that, assuming pairs of words of equal length are generated with equal letter frequencies (that is, each letter in the alphabet is chosen with a probability of 1/26), there is only a one in three chance of discovering the error after ten tests; increasing the number of tests to 20 would still only yield a one in two chance, and one would need to perform over 50 tests to achieve a 90% chance of discovering the error. Finally, and most importantly, there is no certainty that one would ever discover the error, no matter how many tests have been performed. This is a great illustration of how testing can't guarantee correctness. It's easy for someone who isn't a beginner programmer to see why the code is incorrect, but it wasn't obvious to the student; this shows that, like the beginner, if you ever write code that is hard for one of your skill level to write, and which is subtly incorrect, you may never actually realize it without extensive testing, and if it's not extensive enough, you may still never find the bug.