Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

My first verified imperative program

markushimmel.de

Post reply on HN
Print view View original

91–100 of 105 posts

Re: My first verified imperative program

#91

Post by serbuvlad »

lmm wrote: post #57
serbuvlad wrote: post #42

Earlier quoted context omitted.

What's a memory issue? If I access beyond the end of an array in Rust, the panic handler runs and starts unwinding my stack. If I access beyond the end of an array in C++ with .at() the excwption handler runs and starts unwining my stack. If I access beyond the end of an array in C the SIGSEGV handler may (*) run and I could, if I wanted to, start unwinding my stack. Ah, but in C, sometimes if I access the wrong memo…

> Sure, and if I store my data in a Rust array and store indexes into that array around the place as sort of weak references (something I've seen Rust programmers use and talk about all the time), I can easily fetch the wrong data too. Maybe, but you'll do so in an understandable way that you can catch in testing. You won't suddenly start fetching different wrong data when someone builds your program with a newer ver…

> Maybe, but you'll do so in an understandable way that you can catch in testing. You won't suddenly start fetching different wrong data when someone builds your program with a newer version of the compiler, which is a very real risk with C. To say nothing of the risk of arbitrary code execution if your program is operating on attacker-supplied data.

What guarantees it? Literally nothing. You can catch errors in testing in C as well. Yeah, in C you get "different" data on a different version of the compiler, but you get garbage data in all versions of the compiler and Valgrind flags that in testing.

And, of course, you can get arbitrary code execution if your program is operating on data coming from multiple users of different privilege levels in Rust if you use vectors like that.

Sure, Rust fixes a lot of easy to commit bugs in C and C++, absolutely. But there are no absolutes.

Re: My first verified imperative program

#92

Post by MobiusHorizons »

fc417fc802 wrote: post #67
MobiusHorizons wrote: post #58

Earlier quoted context omitted.

What hardware doesn’t use fixed width integers?

A language can provide arbitrary width integers while nonetheless being implemented on top of fixed width integers. In fact I'd say that's pretty typical.

I mean sure, but at that point it's a library, so don't you need to prove the correctness of that library as well?

Re: My first verified imperative program

#93

Post by MobiusHorizons »

Jtsummers wrote: post #59
MobiusHorizons wrote: post #58

Earlier quoted context omitted.

What hardware doesn’t use fixed width integers?

What's the context of your question? Did I say otherwise? Some languages (what's being discussed here) give you arbitrary precision integers, like Lean. So the proof in the blog applies to Lean and any issues with things like -INT_MIN not existing isn't a factor in the proof. That's what's being discussed. The proof for C or Ada or something else with fixed-width integers will be different (and the algorithm, likely)…

> If you knew your target system was using fixed-width integers, you'd use this.

Usually `system` in this context refers to the machine you run the program on, not the language itself, or at least that is how I interpreted it. I guess there used to be systems with BCD math supported by hardware, and I guess those could have variable precision. I'm not sure if it was arbitrary (ie it could still overflow), but one could presumably detect overflow and increase the memory allocation. But once you have a software system doing your math rather than a machine instruction it seems like you need to prove the correctness of that implementation not just the general concept.

Re: My first verified imperative program

#94

Post by lmm »

tsimionescu wrote: post #86
lmm wrote: post #76

Earlier quoted context omitted.

> the terminal accepts certain valid UTF-8 characters (typically from the ASCII subset) as output control characters. This is how you get things like programs that can output colored text. The terminal should not allow such a sequence to break it. Yes, being able to output colour is desirable, but it shouldn't come at the cost of breaking, and doesn't need to. (Whereas it is much less unreasonable for a terminal to b…

I believe you're misunderstanding the problem. The terminal doesn't "break" in the sense that it crashes or does something undefined for those cases. The terminal is doing something that is completely meaningful and well defined and probably has some realistic use cases, such as switching to a different character encoding. The only problem is that it's not what the user wanted to happen. For a simple example, if a fi…

> I believe you're misunderstanding the problem. The terminal doesn't "break" in the sense that it crashes or does something undefined for those cases. The terminal is doing something that is completely meaningful and well defined and probably has some realistic use cases, such as switching to a different character encoding.

I'm aware of the details, but I think sometimes that knowledge leads people to miss the forest for the trees. If the user perceives the terminal as having "broken", that's a case of poor UX design at a minimum. Given that users can readily distinguish between legitimate coloured output etc. and terminals getting into a poor state, it really shouldn't be too hard for the terminal itself to do so. (E.g. it's pretty normal for today's terminals to display some kind of visible warning (complete with resume button) when you press Ctrl-S, rather than simply silently stopping). And while this is a much fuzzier and more contentious claim, I think the Rust community's mentality (as seen in e.g. their approach to compiler errors) nudges people towards such approaches.

Re: My first verified imperative program

#95

Post by lmm »

serbuvlad wrote: post #91
lmm wrote: post #57

Earlier quoted context omitted.

> Sure, and if I store my data in a Rust array and store indexes into that array around the place as sort of weak references (something I've seen Rust programmers use and talk about all the time), I can easily fetch the wrong data too. Maybe, but you'll do so in an understandable way that you can catch in testing. You won't suddenly start fetching different wrong data when someone builds your program with a newer ver…

> Maybe, but you'll do so in an understandable way that you can catch in testing. You won't suddenly start fetching different wrong data when someone builds your program with a newer version of the compiler, which is a very real risk with C. To say nothing of the risk of arbitrary code execution if your program is operating on attacker-supplied data. What guarantees it? Literally nothing. You can catch errors in test…

> What guarantees it? Literally nothing.

The behaviour of looking up index x in array y in rust is well-defined, and consistent between compiler versions. Maybe you use the wrong index and get the wrong customer's data or something, but you'll still get the data at that index (or a panic if the index is invalid).

> You can catch errors in testing in C as well. Yeah, in C you get "different" data on a different version of the compiler, but you get garbage data in all versions of the compiler and Valgrind flags that in testing.

Not always. It's very common for code to be broken according to the standard but do the right thing in some compilers, and then in a different compiler it does something completely bizarre. The code might not do the same thing in testing as it does in release. And while Valgrind does a lot of good for the minority of C programmers who use it, it's far from 100% reliable.

> you can get arbitrary code execution if your program is operating on data coming from multiple users of different privilege levels in Rust if you use vectors like that.

You might in some cases, but it's a lot tricker. You can get the program to operate on different parts of its data than it was intended to, but to go from there to running arbitrary code will still be a significant leap and require an exploitation technique specific to that particular program. Whereas the techniques for going from common classes of C vulnerabilities (e.g. buffer overflow or use after free) to arbitrary code execution are practically textbook at this point.

Re: My first verified imperative program

#96

Post by lmm »

Tainnor wrote: post #84
lmm wrote: post #77

Earlier quoted context omitted.

> Do you realize that making + do what the ordinary mathematical + does, is quite expensive? It requires arbitrary precision arithmetic and hence, potentially, memory allocations. Yes I do. It's an acceptable cost in most cases (you will note much of the world runs on Python, a language in which + does behave sensibly, these days), and dangerous optimisations should be opt-in rather than opt-out. In the worst case yo…

> In the worst case you should at least make your language fail-stop definite by making it error when the result of + is too large rather than silently continuing in an invalid state. That's what Swift does fwiw. But there are downsides to that too (although they're also related to Swift not having a good fault recovery mechanism). In practice, whenever you know you're going to use large enough numbers in Java, you p…

> whenever you know you're going to use large enough numbers in Java, you probably want to use BigInteger or BigDecimal

When you've made a conscious decision you can pick the right thing, sure. The problem usually happens when you haven't thought about it at all, which is why the default should be safe and the unsafe optimisation should be opt-in.

Re: My first verified imperative program

#97

Post by fc417fc802 »

MobiusHorizons wrote: post #92
fc417fc802 wrote: post #67

Earlier quoted context omitted.

A language can provide arbitrary width integers while nonetheless being implemented on top of fixed width integers. In fact I'd say that's pretty typical.

I mean sure, but at that point it's a library, so don't you need to prove the correctness of that library as well?

To the same extent that you need to prove the correctness of the compiler and the language runtime I guess. Arbitrary width integers are a core feature of quite a few languages.

Given Lean's raison d'etre it wouldn't surprise me if the relevant library code was verified. If using another language such as Python I think it would be fairly reasonable to take the underlying implementation on faith. If we're going to start questioning whether a core part of the runtime that implements basic arithmetic operations has bugs then why are we not also suspecting the operations provided by the CPU and other hardware?

We probably should suspect those things, but as a matter of practicality we're going to need a boundary at present.

Re: My first verified imperative program

#98

Post by Tainnor »

lmm wrote: post #96
Tainnor wrote: post #84

Earlier quoted context omitted.

> In the worst case you should at least make your language fail-stop definite by making it error when the result of + is too large rather than silently continuing in an invalid state. That's what Swift does fwiw. But there are downsides to that too (although they're also related to Swift not having a good fault recovery mechanism). In practice, whenever you know you're going to use large enough numbers in Java, you p…

> whenever you know you're going to use large enough numbers in Java, you probably want to use BigInteger or BigDecimal When you've made a conscious decision you can pick the right thing, sure. The problem usually happens when you haven't thought about it at all, which is why the default should be safe and the unsafe optimisation should be opt-in.

But "safe" and "unsafe" are not a binary thing.

Maybe for LOB applications, it would be better if languages defaulted to arbitrary precision arithmetic. But scientific computing is also a huge field that often uses the same languages and there, arbitrary precision is often the completely wrong tool, e.g. it would make certain key algorithms (like Gaussian elimination) exponential.

I feel like this is just one of these things that developers should know about so they can make the correct choice, just like DB indices.

Re: My first verified imperative program

#99

Post by MobiusHorizons »

fc417fc802 wrote: post #97
MobiusHorizons wrote: post #92

Earlier quoted context omitted.

I mean sure, but at that point it's a library, so don't you need to prove the correctness of that library as well?

To the same extent that you need to prove the correctness of the compiler and the language runtime I guess. Arbitrary width integers are a core feature of quite a few languages. Given Lean's raison d'etre it wouldn't surprise me if the relevant library code was verified. If using another language such as Python I think it would be fairly reasonable to take the underlying implementation on faith. If we're going to sta…

Fair enough. I must just not be understanding what the motivation for creating proofs of such software is then. I guess to me assuming the compiler or language runtime have no bugs seem to severely undermine the value of the proof. I feel like if the proof was to have value in an imperative language like C or C++ I would want the assembly proven, as the resulting computation can be drastically altered from the original source text between various compiler flags and optimization levels.

Re: My first verified imperative program

#100

Post by lmm »

Tainnor wrote: post #98
lmm wrote: post #96

Earlier quoted context omitted.

> whenever you know you're going to use large enough numbers in Java, you probably want to use BigInteger or BigDecimal When you've made a conscious decision you can pick the right thing, sure. The problem usually happens when you haven't thought about it at all, which is why the default should be safe and the unsafe optimisation should be opt-in.

But "safe" and "unsafe" are not a binary thing. Maybe for LOB applications, it would be better if languages defaulted to arbitrary precision arithmetic. But scientific computing is also a huge field that often uses the same languages and there, arbitrary precision is often the completely wrong tool, e.g. it would make certain key algorithms (like Gaussian elimination) exponential. I feel like this is just one of thes…

> arbitrary precision is often the completely wrong tool, e.g. it would make certain key algorithms (like Gaussian elimination) exponential.

Sure, but even in science taking a lot of time to deliver a result, or failing to deliver one at all, is much safer than silently delivering the wrong result. There's the concept of fail-stop if you want a rigorous approach to safety. There's no analogous safety model that says silent overflow is the safe option.

Post reply on HN