Hacker News Reader

Comment by anonzzzies | Hacker News Reader

> it is understanding how systems interact and their performance characteristics.

But there is, at least a theoretical, promise that when you are rigid enough in your types, you are able to predict & prove memory, cpu, network use etc. It's pie in the sky, especially for interacting systems, but there is some future to cling on to. When doing embedded work, I use some of these to make sure algorithms stay within the limits in a way that they won't compile if they don't.

There are also provable security which I also use (sparingly). We will get there, hopefully before I give up coding and become a fultime carpenter.

View on HN

> But there is, at least a theoretical, promise that when you are rigid enough in your types, you are able to predict & prove memory, cpu, network use etc.

No, that’s not even theoretically possible in the general case, see Rice’s theorem (at least if you stick to Turing complete programs), which states that every non-trivial (semantic) property of a program is undecidable.

Rice's theorem states that there is no general procedure to determine if an arbitrary Turing machine has some property. We are restricting ourselves to programs which typecheck under a certain type system, so there will certainly be a class of properties it can guarantee while still being Turing-complete (such as the bounding of memory, CPU, etc.). That is to say that it's not "theoretically possible in the general case," but we are willing to work with more specific cases, so it's not relevant to invoke Rice's theorem in this situation.

> such as the bounding of memory, CPU

I don’t think any of those are possible (given that there is some construct in the language which will grow the memory) - how do you discern how many times will a given loop run?

For example, how much memory does this program use?

  int x = input().toInt()

  for 0..x {
    // something that allocates at least until the end of the loop
  }

And this is the very nicest case of a statically verifiably not infinite loop!

It's not verifiable because you're trying to prove an incorrect spec! This program's memory usage is _not_ bounded above by a constant!

However, many modern formal methods _could_ prove that this function uses `f(x)` space, provided the loop body is simple enough.

For the case of resource usage, you can see work like https://link.springer.com/chapter/10.1007/978-3-030-81685-8_... "Synthesis with Asymptotic Resource Bounds" which implements bounded resource checking. Of course, there are programs it rejects that it can't prove, but this is the essence of type systems: if you are willing to appease the typechecker, then you can establish facts about runtime properties.

For your case, there may be a simpler dependently-typed solution: in such systems, you can already say things like "given an input natural number n determined at runtime, this functions returns a vector of size n", which bounds the result vector size. One approach could be to disallow explicit memory allocation and require passing a memory allocator as a parameter along with the associated "request" number bounding how many allocations you can do, in a similar dependently-typed way.

Proofs do not have to be of the form "This will never use more than 64 bytes of memory". You can prove that something will use x times 32 bytes of memory, or a polynomial value based on x, or whatever you have. Then you have to decide if that meets your needs or not.

But this is also where they get tricky. You can have a proof that a particular sort function will never use more than twice the memory of what you pass in, and then you can combine that with a proof that some other bit of code will never have more than 10 elements, and that produces a proof that you only need 20 element's worth of memory for that upper function... but across an entire program, what sounds cute and useful in my little example here becomes its own monster of complexity. So far it is not yet clear to me that it constitutes an improvement on the underlying program.

I'm going to assert, you can calculate how much memory you'll need as soon as you see x. (maybe it's gnarly and complicated, but you can put an upper bound on it).

That number can be calculated at runtime. The program has access to the number, and you can make a choice about running that for loop or not.

The nifty bit is, the memory use information can be encoded in the type. the function has access to its type information. The compiler checks, and can make guarantees about your guard strategy - the actual values of available memory, and how much memory operating on x requires are only known at runtime. But the compiler can be check at compile time that the strategy is sound. maybe you have 5 bytes, maybe you have 5 gigs, who cares?

This can all be done without fancy languages, just write good code.

It's pretty nice to be able to throw more allocating function calls in the for loop, and have the compiler recognize that you're using (maybe) more memory, but your guard strategy is still good.

I think you're being overly reductive:

> Using Rogers' characterization of acceptable programming systems, Rice's theorem may essentially be generalized from Turing machines to most computer programming languages: there exists no automatic method that decides with generality non-trivial questions on the behavior of computer programs.

https://en.wikipedia.org/wiki/Rice%27s_theorem

I don't understand why you say that my comment is reductive. It's adding nuance to the topic at hand, rather than removing it. The original comment talks about a situation where we constrain ourselves to "rigid types"; the child comment remarks on Rice's theorem having consequences for the analysis of general Turing machines; and I remind the commenter that we have already restricted ourselves to Turing machines satisfying some type system.

Another way to express the same point of view is to say that I am arguing that the Curry-Howard isomorphism is more relevant to the situation at hand than Rice's theorem. (This might be the "promise" that the original commenter was referring to.)

This is a good but also misunderstood point. It is true that you can't automatically do this in general. However, expressive enough type systems can contain human-written, machine-checked proofs of (models of) these properties. I think the jury's still out on whether or not humans or machines are better at coming up with proofs, but computers are decisively a lot better at checking them than we are.

The way I see it formal methods not a holy grail where we don't have to think about the code we're writing anymore, but it is a very strong next step from "I wrote this code and here's why I think it's right" to "I wrote this code and here's a machine-checked proof that it's right". Effective automation can make that step easier to take in a lot of real-world cases.

It’s not about automatically doing it — it’s about for many cases there can’t exist a proof. And it is not even some theoretically interesting but never happening case, but quite trivial programs will quickly come to this state. Sure you can restrict some things, like boundless loops, but the “beauty” of complexity and the limit of our very mathematics won’t disappear, unless you go to too trivial systems which are useless. See my other comment for an example.

I remember there being an analogy between Gödel’s incompleteness theorem as well, which is also only true to “expressive enough” systems (where you can basically do integer math) — but I may be talking completely out of my arse at this point.

I get your point, and I agree with it too. My comment is (trying to) say that in those cases we don't know that humans are any better!

Your other comment has some problems, but a better example is

fn collatz(mut n: bigint, mut v: Vec<...>) {

  loop {

     n = { if n%2==0 then n/2 else 3\*n+1 };

     v.push(...);

  }

}

As far as we know, we can't bound the memory usage of this program: and if any FM can do it as well then there's a million bucks on the table. But so far no human can do it either! And if your program relies on this program using bounded memory, from an engineering perspective you're kind of SOL no matter what.

On the other hand, if you're writing programs which humans are pretty sure they know why the properties they want hold (as we usually try to do, anyways), then translating this into a machine-checked proof can give you a lot more faith that the property actually holds and possibly even find flaws in your reasoning/implementation if there are any!

Yes I agree with you on every point (though didn’t want to use the “heavy gunner” Collatz as an example :D). I’m not against dependent types, and I eagerly await what future might they bring. But at the same time I think the best solution will be to “fight on multiple fronts”, and improve our type and test systems. There are very interesting ways to systematically test every kind of input (greatly reducing the input space) that has a distinct code path (and it can find a minimal reproducible error case!).

Well one thing programmers do often due to the complexity of formal proof is random property testing instead. Mathematicians do so too, which is why the Collatz conjecture is a conjecture in the first place. There is an alternative to Software Foundations that uses randomized property checking. It would be interesting to have a hybrid system where we independently give specifications and then decide whether we wanted to formally prove them or just do tests instead.

"(at least if you stick to Turing complete programs)"

Many people interesting in this sort of formal proof community are actually perfectly willing to eject that. There's been a lot of interesting research into it. I think you can also ring-fence chunks of a program as being non-Turing complete and prove things about those chunks even if the program as a whole is Turing complete.

That said, so far everything I've seen them produce involves a level of programming difficulty comfortably above writing real-world code in Haskell. For example, you do not have to learn category theory in the slightest to learn Haskell, but you will be learning a lot of real mathematical theories, of which group theory is probably one of the easier ones, to use these systems. They're working on that issue. But it has a long ways to go and it is not clear to me that the gap between these systems and the "programmer on the street" is anything that can ever be solved.

Or, to put it another way in more engineering terms, I do not question the advertised benefits when advocates like the original author pitch them. They're real and exist in real, concrete systems that you can use today. However, the costs are grotesquely undersold. I'm not sure even the advocates really understand how far out of the loop they are on the costs of their systems. So far the costs end up choking you out on systems that conventional programmers would consider tiny. My browser may not be mathematically proved to not have security vulnerabilities, and it's certainly not free of bugs, but in the meantime, conventional programming has produced it and it's out there in the world bringing benefits today, not in however many decades or even centuries we are away from having something like a browser-sized program come with proofs of security and resource usage.

Type systems push semantic properties into syntactic ones, thereby making them decidable. Note that there are halting programs which will fail to type check, but that’s the trade off.

> Type systems push semantic properties into syntactic ones

Ordinary types are so-called trivial properties though, so Rice’s theorem doesn’t apply to them.

You can get a lot better than trivial. Transactions for instance.

This isn't right: `int -> Zero` is an "ordinary" type, but certainly does not correspond to a trivial property. The reason Rice's theorem doesn't apply to types is that they're not purely "semantic" in the relevant sense, since they're not fully determined by the language a TM accepts.

What type system do you imagine having that type signature? Zero being a value is usually exempt from the type system (unless we have dependent types, but I would definitely not call those ordinary). Of course if it’s a special type with only a single elem with no relation to int, then it is again trivial.

Any language with function types and singletons.

> Of course if it’s a special type with only a single elem with no relation to int, then it is again trivial.

No, it isn't. "Trivial" in the context of Rice's theorem means either true of all Turing machines or false of all Turing machines.

Typed Racket (not a dependently typed system mind you) has zero as a type. It’s a fantastically useful type to have.

The general case is for arbitrary programs. That's not the important case. You want to prove things about _this_ program which you've written, not about all programs.

I think you are on the path that is how this will actually be used: It gets added in little bits.

I could be rigid enough with my types to prove more than I do. I don't because the payback isn't worth the effort. When it is worth the effort, then people will (gradually start to) use it.

> When doing embedded work, I use some of these to make sure algorithms stay within the limits in a way that they won't compile if they don't.

Could you be a bit more specific here about what you do, why you do it in embedded (and not elsewhere), what it protects you from, and how it does so?

> Could you be a bit more specific here about what you do, why you do it in embedded (and not elsewhere), what it protects you from, and how it does so?

We create, upgrade, maintain, validate applets for emv and other cryptographic and sensitive embedded (MCUs) applications; I try to guarantee safety using tla+, coq, z3 and agda. Or just on paper. And we deliver that as paper with our software.

It’s just some functions, not all: we often have to, because of certification, show ‘a story’ (not proof) that things will be ‘secure enough’. I personally enjoy it more to prove some of the crucial parts as ‘the story’ not write a story.

Reply on news.ycombinator.com