Hacker News Reader

Comment by dilippkumar | Hacker News Reader

From https://chaos-lang.org/docs/11_decision_making

> Decision making(a.k.a. control structures) in Chaos language is only achievable on function returns for the sake of zero cyclomatic complexity.

...

> At first glance, defining the control structures in this way might seem so unnecessary or inconvenient but this is the pinnacle of writing 100% testable, clean and error-free code in any programming langauge by far.

I’m skeptical about this claim. I’m not sure I believe 100% error-free is possible in any language.

Can someone please elaborate on this claim?

View on HN

I agree with the other commenter about the comma in this sentence. But I'd also like to point out that 100% error-free code is possible. There's a whole branch of computer science dedicated to it: formal verification. I personally have used Coq to write certified code in the past, and I'm quite confident that my code was 100% error-free.

Of course, there are some qualifications one should make regarding such a claim: you have to trust that your specification is "correct", that your hardware is functioning correctly, that the proof checker didn't accept a bogus proof, that the underlying logic (e.g., the calculus of inductive constructions) is consistent, etc. That's a lot of things to trust, but the point is that you don't have to trust yourself.

I really can't trust myself to write a specification. I know this because I have written errors in tests before - even when all I'm doing is trying to work out some properties that the answer ought to have, I can still make a mistake. It's just usually less likely that I would make a mistake, because the specification is simpler than the algorithm.

So, it is not really fair to downplay the chance that you could have a wrong specification, although it would be equally wrong to use that as an excuse to downplay the value of Coq.

WPA2 is a formally verified protocol. It lasted 14 years: https://www.krackattacks.com/. Now it's partially formally verified.

You can't prove that something is secure, because to be applicable in mathematics/computer science there has to exist a precise definition.

If someone is just saying "This is a formally verified protocol" without what they actually checked for, they are salespeople not mathematicians.

"The authors of the KRA paper were able to understand what the proofs were about, and why they don’t cover the KRACK vulnerability. Even though the original proofs didn’t reveal security flaws, a principled approach would use these proofs in order to discover where to look."

https://galois.com/blog/2017/10/formal-methods-krack-vulnera...

If it's impossible to write anything you're guaranteed to not have any errors.

I don't think '100%' distributes over commas in this case, especially given the formatting in the original

I mean yes it's either obviously wrong or hyperbole, I assume the second.

But I think the idea is that by forcing each branch in a case to be an separate function they are forced to be unit testable.

But then any more or less complex code that involves conditions will be spread over multiple functions. Even if that makes it testable, it might become incomprehensible very quickly.

Edit: If code needs certain number of conditions, they will be there in this or that form, that cannot be avoided. I would like to see real benefits of their choice in real non-trivial examples.

"100%" only qualifies "testable".

That sounds.... chaotic

Reply on news.ycombinator.com