5 ms·

SAT solvers are fun. Math is fun. Neither is the most important part of development. Most of my time is not spent formally testing these methods; it is unders

SAT solvers are fun. Math is fun. Neither is the most important part of development. Most of my time is not spent formally testing these methods; it is understanding how systems interact and their performance characteristics. I disagree with OP's assertion about legacy languages; they have largely focused their improvements on the areas that actually matter to my day to day development.

anonzzzies 3y ago
> 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.
- AnimalMuppet 3y ago
  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?
  - anonzzzies 3y ago
    > 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.
- kaba0 3y ago
  > 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.
  - arxanas 3y ago
    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.
    - kaba0 3y ago
      > 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!
      - markusde 3y ago
        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.
      - arxanas 3y ago
        For the case of resource usage, you can see work like https://link.springer.com/chapter/10.1007/978-3-030-81685-8_37 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.
pharmakom 3y ago
> how systems interact and their performance characteristics Let’s bring these aspects into the fold of mathematical modelling then.
mpweiher 3y ago
Yeah, I am also deeply indifferent to these things, even if a part of me says "cool". We have largely solved programming-in-the-small. Making it a little bit better is not horrible, but just doesn't move the needle much if at all. And you have to consider whether the costs are worth it. I do think that focusing on these things detracts from the bigger problems we need to solve.

anonzzzies 3y ago

> 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.

AnimalMuppet 3y ago
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?
- anonzzzies 3y ago
  > 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.
kaba0 3y ago
> 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.
- arxanas 3y ago
  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.
  - kaba0 3y ago
    > 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!
    - markusde 3y ago
      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.
    - arxanas 3y ago
      For the case of resource usage, you can see work like https://link.springer.com/chapter/10.1007/978-3-030-81685-8_37 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.

pharmakom 3y ago

> how systems interact and their performance characteristics Let’s bring these aspects into the fold of mathematical modelling then.

mpweiher 3y ago

Yeah, I am also deeply indifferent to these things, even if a part of me says "cool". We have largely solved programming-in-the-small. Making it a little bit better is not horrible, but just doesn't move the needle much if at all. And you have to consider whether the costs are worth it. I do think that focusing on these things detracts from the bigger problems we need to solve.