undefined | Better HN

0 pointspron1y ago0 comments

> This is a strawman fallacy, we're not talking purely theoreticals.

No, this is the technique we use in practice in formal methods to prove program properties. When we write a program correctness proof in TLA+ or Lean, this is what we do. This is also how we build invariants into languages. When you learn how to write formal proofs and design type systems, this is what you learn.

> Rust, however, can maintain invariants and be expressive enough because it relies on outside the computer assistance (aka unsafe blocks).

Rust maintains its invariants by making a stronger invariant inductive in the language.

> Google mentioned they had little problem getting people to work with Rust.

I am not talking about Rust in particular. I'm talking about your general point that more soundness is always better, and your claim that my argument is an example of a nirvana fallacy because I compare an imperfect solution to a hypothetical perfect one. I am trying to explain that we know that more soundness is sometimes worse for correctness in practice. The problem is not that more soundness isn't perfect, but that there are currently better solutions than more soundness in some situations.

You seem to be unaware of the shift in software correctness since the seventies. The gap between the size of programs we can prove correct using deductive methods (currently ~10KLOC) and the size of programs produced in industry is only growing. That is why there's been a shift from deductive proofs to methods such as concolic testing (e.g. KLEE). You can see that by looking at the programs for any software verification / formal methods conference.

To be clear, I am not saying that more soundness is never better; I'm saying it is sometimes worse. You can say that we should use ATS more, but the effort of producing software that's proven correct with ATS is not justified by the additional correctness guarantees you gain. I.e., at some point you pay $1000 for improved confidence worth $100.

0 comments

3 comments · 1 top-level

Ygg21y ago· 2 in thread

> No, this is the technique we use in practice in formal methods to prove program properties

A program that can't express H (72 in decimal) in Hello world is about as divorced from practicals as you can get, without mixing String theory, Meth and Math.

> Rust maintains its invariants by making a stronger invariant inductive in the language.

Yes, but it relies very little on human verification.

> I'm saying it is sometimes worse.

And I'm saying it as a programmer field we should monotonically approach the ideal by removing languages that don't support it. A language that has memory safety issues is worse than a language that doesn't. We had hundreds of example in practice where people just can't write/compose safe code.

C has a 50 year history and most of the active projects in it are mired in memory safety issues.

Also seatbelts are sometimes worse, doesn't mean we shoud abolish them for seatbelts-less Pintos.

pronOP1y ago

> A program that can't express H (72 in decimal) in Hello world is about as divorced from practicals as you can get

Huh? I was giving an example of how we make undecidable properties trivial in languages. It can be any property. It's easy to see that Rust does the same with memory safety, i.e. through an inductive invariant, because every statement in Rust maintains the invariant.

> Yes, but it relies very little on human verification.

Of course. It shouldn't rely on human verification at all. That's how we design type systems. But because an inductive invariant is inherently conservative and must reject correct programs, there is additional human effort required -- not to verify the property, but to stay within the confines of the inductive invariant. In Rust terms, the compiler takes care of memory safety, but you need to put an effort into expressing memory-safe programs in Rust to fit within Rust's constraints, which are, necessarily more restrictive than memory safety (because they must use an inductive invariant).

> And I'm saying it as a programmer field we should monotonically approach the ideal by removing languages that don't support it.

And I'm saying that what we've learnt over the past five decades is that more soundness does not necessarily mean getting closer to the ideal. Sometimes more soundness gets us further away from the ideal.

> Also seatbelts are sometimes worse, doesn't mean we shoud abolish them for seatbelts-less Pintos.

No one is suggesting that, it's just that what you're referring to as seatbelts could sometimes do more harm than good even for safety. We have empirical evidence that real seatbelts increase safety; things are nowhere near as clear for language soundness.

Sure, C is so exceptionally weak that we can do better than that, and there's no doubt Rust is better on correctness than C, but that's not the same as saying Rust is better on correctness than any language that makes fewer guarantees than Rust. Why? Because, again, we've seen that the benefits of soundness are not linear -- they help until they start hurting. Knowing where that point is is not easy.

Ygg21y ago

> Huh? I was giving an example of how we make undecidable properties trivial in languages. It can be any property.

Yes, but insisting you have to be 100% machine verified, while the program is correct, it is impractical. While it might be Turing complete, it can't express equivalent behavior to a C program.

This is one of those quotes like "Don't let perfect be the enemy of good".

Look at your definition of memory safety, by it nothing other than ATS or some Lisp derivative running on a Lisp machine is actually memory safe.

Sure, it's theoretically sound, but it's not pragmatical.

> We have empirical evidence that real seatbelts increase safety; things are nowhere near as clear for language soundness.

We have empirical evidence that Rust has measurable impact on bugs, especially memory safety ones.

1 more reply

j / k navigate · click thread line to collapse