7 ms·

Mathematical proofs of code are not suitable for most systems. Even unit tests which don't involve proofs can be a problem sometimes because they lock down API

Mathematical proofs of code are not suitable for most systems. Even unit tests which don't involve proofs can be a problem sometimes because they lock down API inputs and outputs. It's already a major problem when a developer wants to change some code and they have to spend hours updating unit tests every time. When in small teams, heavy 100% coverage unit tests slow down productivity, possibly by 5x or 10x. I imagine that adding proofs as part of the unit test suite would further increase the productivity cost overhead by a massive factor. In software development, you should avoid treating the code like if it's special or perfect because it's not and it will need to be changed in the near future when requirements change (and they will always keep changing). So locking it down into a specific state with proofs all around it is a bad idea for the vast, vast majority of cases. We need more wisdom in software development and that means taking a step back, looking at the big picture and asking questions like what are the negative side effects of each new methodology that we are introducing into our projects? There are always downsides, and we're crazy to pretend that every fancy new methodology is a silver bullet.

hmottestad 9y ago
It's hard to know the intent of a developer by reading their code. You could always add a bunch of comments, which would help, but in the long run you risk them getting out of date. My unit tests are basically "comments" for my code, that show me how the code is supposed to work. When I make changes, the tests will tell me if I broke the intentions of the initial developer. Sure, when doing big changes, just updating and maintaining the tests is a lot of work, but so would maintaining documentation and comments be. So we have less documentation and fewer comments, and more tests.
- jondubois 9y ago
  I find integration tests more useful for documentation because they show you how the system works at a higher level which is precisely what new developers need to understand. If the code itself is written properly then the individual classes and objects used throughout should be high cohesion and easy to read without needing any comments or tests. There are always cases where unit tests are important though like the parts of the code that deal with money. But there is no benefit in adding unit tests if you're building a standard chat system for example; integration tests are sufficient in that case. Also getting 100% test coverage is a complete waste of time if you don't actually test the right kinds of input and output parameters.
  - hmottestad 9y ago
    Integration tests are much more brittle in my experience. A simple test for doing frontend/backend integrations tests with web driver can easily break due to race conditions or changes in other parts of the system. Such tests are great for detecting that something is wrong, but it can be very hard to figure out what's wrong and where things went wrong. Had a lot of "fun" rewriting a bunch of integration tests for angular, because the framework used a lot of Promises which caused race conditions. Those tests were much harder to write than unit tests and were much easier to mess up.
    - jondubois 9y ago
      They're not necessarily brittle but I know what you mean. When the integration tests reach across multiple services then things tend to get brittle but this can be fixed by stubbing out the external services. Stubs are not just useful for unit tests. Service stubs are often much easier to write than module stubs because services often communicate via string based protocols which are easy to simulate.
    - crdoconnor 9y ago
      >Integration tests are much more brittle in my experience. In my experience brittleness in tests is caused by bugs in tests or bugs in code. Most of these things can be fixed, e.g. * Add an order by to select statements that otherwise returns data in an indeterminate order. * Fix the interpreter/database version you are using to run your code rather than relying upon the version the package manager has installed. * Stub out code that gets date/time/random numbers. * Stubbing out external APIs which go down on Tuesdays. * Fixing the bugs in your code. * Abandoning the code you rely upon which is buggy (I'm just sayin', angular might not be the ideal framework). Avoiding writing these tests because you know that "they'll be too buggy" doesn't exactly send out a great signal. >Such tests are great for detecting that something is wrong, but it can be very hard to figure out what's wrong and where things went wrong. This is alleviated by integrating debugging tools into your test environments.
  - zxcmx 9y ago
    I think a part of the difficulty is in the language of coverage. "100% test coverage" usually means statement coverage due to the nature of popular tooling. If you deeply care about correctness you are usually more interested in path coverage which is more tied to things like heap shape or state space... (which depending on your system design might encompass stuff in your database). Also yeah, technically the exceptions which can be thrown at each point in your software if you work in a language with those. Unfortunately there's not much tooling for that so it's not visible in the same way as the more naive metrics. Anway my point is that you can waste time pushing for "100% statement coverage" measurable by naive tools but still not exercise important paths, which I think is your point.
- pmontra 9y ago
  Recently I found a get_info(doc) which was hard to understand. It should have been get_xrsf_token(web_page) which would have been self explanatory. I mostly develop backends of web apps. In my experience not every web app has some code that needs to be explained. Picking the correct names is usually enough. That said, unit tests really do what you write: provide examples, use cases and guidance.
- z3t4 9y ago
  I find the best approach is the keep the code base small enough so you can keep everything in your head. Knowing that if you change something you also have to update this and that , and make sure feature x, y, z still works (which could be done with automated tests).
mauricioc 9y ago
The presentation addresses this in a way. The argument is that in Coq you can write proof _scripts_ ("repeat this simplification operation until it does nothing", "pattern match on this definition and apply this operation to every subcase", "proof tactics" and so on), and in this way the same proof script can prove different theorems. So there is a possibility that changing the code only forces you to change theorem statements (that is, the spec), allowing reuse of the proof script itself. Now you are doing software engineering on proof scripts, and you face the same generality/flexibility problems you would face when writing unit tests. A well-written proof script would be flexible enough, and a hacky one would lock things down too much.
- bsaul 9y ago
  That part made me wonder if a day will come where some generic script would be able to work with any theorem on any code, maybe with the help of some kind of introspection ( at this level of abstraction i’m not even sure introspection is the right concept).
  - deleted 9y ago
    [deleted]
  - firethief 9y ago
    Short answer: no. Long answer: https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_... There cannot be a program that can prove (or even help a human to prove) any true statement about programs written in a Turing-complete language.
    - bsaul 9y ago
      As always with this theorem it's pretty hard to be sure if the kind of non provable statement happen often enough to be a concern in practice
    - hackinthebochs 9y ago
      But most code isn't using the features that make Turing complete languages messy, i.e. evolving the executable code as executing progresses. Most real-world code exists in a subset of Turing complete languages where generic theorem proving could probably work.
jononor 9y ago
Test primarily against external APIs. Those should be stable against change anyways, so that the external consumers can rely on it. Generally don't test against internals much, except if an area is shown to be buggy and hard to exercise externally. Prefer (well tested) libraries for generic functions/algorithms. If you have to implement one, put tests on it as if it was external API. Consider publishing it independently to make it external. If needs change, just drop the dependency.
KirinDave 9y ago
> Mathematical proofs of code are not suitable for most systems. It depends what kind of math and what they're doing though. Systems like Coq give you much more trustable code to put in your system, and higher degrees of trust for clients. But systems like Idris actually let you write code and use the proof engine to write trustworthy code. Most of that "math", from the perspective of a programmer, is a small subset of graph theory, formal logic, and category theory useful for proving relationships and reflexivity so that the machine can help you. > Even unit tests which don't involve proofs can be a problem sometimes because they lock down API inputs and outputs. This is a much bigger problem than "hand written mocks are bad" (which they are, I agree). But it's quite out of scope to complain that because API endpoints are often sloppily deployed without versioning or introspectability, that all formal methods are wrong. What's more, and I really want to push this point so I'll emphasize it: quickly producing broken code helps almost no one. If you're an artist playing with making a synthesizer whine? Maybe okay. If you're writing software intended to face the world and do real work? We can't just keep pretending we're all smart enough to do this without mechanical aid; we're NOT smart enough to do this without mechanical aid anymore. Programs integrate too many libraries and APIs. > I imagine that adding proofs as part of the unit test suite would further increase the productivity cost overhead by a massive factor. With Idris, it makes it so the program can write code for you. I've been learning it over the last 2 weeks and I'm totally fascinated by how much drudgery it takes out of total programming. > In software development, you should avoid treating the code like if it's special or perfect This is precisely what formal methods do! You challenge every piece of code you can and say, "Prove to me that what you've written doesn't have an obvious flaw!" You rewrite until both the human and the proof engine cannot see anymore. It is not sacred at that point (no one believes this), but at least you've acknowledged that you can write errors and started to mitigate them. > There are always downsides, and we're crazy to pretend that every fancy new methodology is a silver bullet. Actually, the entire industry has started to demand that developers do a lot more computation on their ends to make better software. The "prove more of your program and write total code" is just one side of the "do more work on your end" school. Another is, "Your software is in fact the output of this algorithm training from a dataset on 4 GPUs." We probably need a similar step forward for APIs (where APIs are invalid & unusable without a spec that governs them). It is a change, but most commercial software engineers are handling user data that can be leveraged in disastrous every day. As you say, we need the wisdom to realize that it's difficult to guess the use case or security impact of the code we write on a daily basis, and we need to start taking that fact seriously. These heady days of being able to deny responsibility and shove out any software we want without consequence need to end.
adultSwim 9y ago
Re-think your assumptions about "mathematical proofs". Compiling software with types is a mathematical proof. We get certain guarantees "for free" without even thinking about it. It's immensely useful and flexible. We can build better type systems than are in common use. So much more is possible than just making sure we don't stick an int where a string is supposed to go. Moving forward is about raising the bar on what we get "for free". We have a lot of experience building programs that help us program (e.g. compilers, IDEs, build systems) We can move forward without falling into traps (low performance, high programmer knowledge required, overly rigid, more work required than gained in productivity) There are no silver bullets but we can continue to improve.

hmottestad 9y ago

It's hard to know the intent of a developer by reading their code. You could always add a bunch of comments, which would help, but in the long run you risk them getting out of date. My unit tests are basically "comments" for my code, that show me how the code is supposed to work. When I make changes, the tests will tell me if I broke the intentions of the initial developer. Sure, when doing big changes, just updating and maintaining the tests is a lot of work, but so would maintaining documentation and comments be. So we have less documentation and fewer comments, and more tests.

jondubois 9y ago
I find integration tests more useful for documentation because they show you how the system works at a higher level which is precisely what new developers need to understand. If the code itself is written properly then the individual classes and objects used throughout should be high cohesion and easy to read without needing any comments or tests. There are always cases where unit tests are important though like the parts of the code that deal with money. But there is no benefit in adding unit tests if you're building a standard chat system for example; integration tests are sufficient in that case. Also getting 100% test coverage is a complete waste of time if you don't actually test the right kinds of input and output parameters.
- hmottestad 9y ago
  Integration tests are much more brittle in my experience. A simple test for doing frontend/backend integrations tests with web driver can easily break due to race conditions or changes in other parts of the system. Such tests are great for detecting that something is wrong, but it can be very hard to figure out what's wrong and where things went wrong. Had a lot of "fun" rewriting a bunch of integration tests for angular, because the framework used a lot of Promises which caused race conditions. Those tests were much harder to write than unit tests and were much easier to mess up.
  - jondubois 9y ago
    They're not necessarily brittle but I know what you mean. When the integration tests reach across multiple services then things tend to get brittle but this can be fixed by stubbing out the external services. Stubs are not just useful for unit tests. Service stubs are often much easier to write than module stubs because services often communicate via string based protocols which are easy to simulate.
  - crdoconnor 9y ago
    >Integration tests are much more brittle in my experience. In my experience brittleness in tests is caused by bugs in tests or bugs in code. Most of these things can be fixed, e.g. * Add an order by to select statements that otherwise returns data in an indeterminate order. * Fix the interpreter/database version you are using to run your code rather than relying upon the version the package manager has installed. * Stub out code that gets date/time/random numbers. * Stubbing out external APIs which go down on Tuesdays. * Fixing the bugs in your code. * Abandoning the code you rely upon which is buggy (I'm just sayin', angular might not be the ideal framework). Avoiding writing these tests because you know that "they'll be too buggy" doesn't exactly send out a great signal. >Such tests are great for detecting that something is wrong, but it can be very hard to figure out what's wrong and where things went wrong. This is alleviated by integrating debugging tools into your test environments.
- zxcmx 9y ago
  I think a part of the difficulty is in the language of coverage. "100% test coverage" usually means statement coverage due to the nature of popular tooling. If you deeply care about correctness you are usually more interested in path coverage which is more tied to things like heap shape or state space... (which depending on your system design might encompass stuff in your database). Also yeah, technically the exceptions which can be thrown at each point in your software if you work in a language with those. Unfortunately there's not much tooling for that so it's not visible in the same way as the more naive metrics. Anway my point is that you can waste time pushing for "100% statement coverage" measurable by naive tools but still not exercise important paths, which I think is your point.
pmontra 9y ago
Recently I found a get_info(doc) which was hard to understand. It should have been get_xrsf_token(web_page) which would have been self explanatory. I mostly develop backends of web apps. In my experience not every web app has some code that needs to be explained. Picking the correct names is usually enough. That said, unit tests really do what you write: provide examples, use cases and guidance.
z3t4 9y ago
I find the best approach is the keep the code base small enough so you can keep everything in your head. Knowing that if you change something you also have to update this and that , and make sure feature x, y, z still works (which could be done with automated tests).

mauricioc 9y ago

The presentation addresses this in a way. The argument is that in Coq you can write proof _scripts_ ("repeat this simplification operation until it does nothing", "pattern match on this definition and apply this operation to every subcase", "proof tactics" and so on), and in this way the same proof script can prove different theorems. So there is a possibility that changing the code only forces you to change theorem statements (that is, the spec), allowing reuse of the proof script itself. Now you are doing software engineering on proof scripts, and you face the same generality/flexibility problems you would face when writing unit tests. A well-written proof script would be flexible enough, and a hacky one would lock things down too much.

bsaul 9y ago
That part made me wonder if a day will come where some generic script would be able to work with any theorem on any code, maybe with the help of some kind of introspection ( at this level of abstraction i’m not even sure introspection is the right concept).
- deleted 9y ago
  [deleted]
- firethief 9y ago
  Short answer: no. Long answer: https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems https://en.m.wikipedia.org/wiki/G%C3%B6del's_incompleteness_... There cannot be a program that can prove (or even help a human to prove) any true statement about programs written in a Turing-complete language.
  - bsaul 9y ago
    As always with this theorem it's pretty hard to be sure if the kind of non provable statement happen often enough to be a concern in practice
  - hackinthebochs 9y ago
    But most code isn't using the features that make Turing complete languages messy, i.e. evolving the executable code as executing progresses. Most real-world code exists in a subset of Turing complete languages where generic theorem proving could probably work.

jononor 9y ago

Test primarily against external APIs. Those should be stable against change anyways, so that the external consumers can rely on it. Generally don't test against internals much, except if an area is shown to be buggy and hard to exercise externally. Prefer (well tested) libraries for generic functions/algorithms. If you have to implement one, put tests on it as if it was external API. Consider publishing it independently to make it external. If needs change, just drop the dependency.

KirinDave 9y ago

> Mathematical proofs of code are not suitable for most systems. It depends what kind of math and what they're doing though. Systems like Coq give you much more trustable code to put in your system, and higher degrees of trust for clients. But systems like Idris actually let you write code and use the proof engine to write trustworthy code. Most of that "math", from the perspective of a programmer, is a small subset of graph theory, formal logic, and category theory useful for proving relationships and reflexivity so that the machine can help you. > Even unit tests which don't involve proofs can be a problem sometimes because they lock down API inputs and outputs. This is a much bigger problem than "hand written mocks are bad" (which they are, I agree). But it's quite out of scope to complain that because API endpoints are often sloppily deployed without versioning or introspectability, that all formal methods are wrong. What's more, and I really want to push this point so I'll emphasize it: quickly producing broken code helps almost no one. If you're an artist playing with making a synthesizer whine? Maybe okay. If you're writing software intended to face the world and do real work? We can't just keep pretending we're all smart enough to do this without mechanical aid; we're NOT smart enough to do this without mechanical aid anymore. Programs integrate too many libraries and APIs. > I imagine that adding proofs as part of the unit test suite would further increase the productivity cost overhead by a massive factor. With Idris, it makes it so the program can write code for you. I've been learning it over the last 2 weeks and I'm totally fascinated by how much drudgery it takes out of total programming. > In software development, you should avoid treating the code like if it's special or perfect This is precisely what formal methods do! You challenge every piece of code you can and say, "Prove to me that what you've written doesn't have an obvious flaw!" You rewrite until both the human and the proof engine cannot see anymore. It is not sacred at that point (no one believes this), but at least you've acknowledged that you can write errors and started to mitigate them. > There are always downsides, and we're crazy to pretend that every fancy new methodology is a silver bullet. Actually, the entire industry has started to demand that developers do a lot more computation on their ends to make better software. The "prove more of your program and write total code" is just one side of the "do more work on your end" school. Another is, "Your software is in fact the output of this algorithm training from a dataset on 4 GPUs." We probably need a similar step forward for APIs (where APIs are invalid & unusable without a spec that governs them). It is a change, but most commercial software engineers are handling user data that can be leveraged in disastrous every day. As you say, we need the wisdom to realize that it's difficult to guess the use case or security impact of the code we write on a daily basis, and we need to start taking that fact seriously. These heady days of being able to deny responsibility and shove out any software we want without consequence need to end.

adultSwim 9y ago

Re-think your assumptions about "mathematical proofs". Compiling software with types is a mathematical proof. We get certain guarantees "for free" without even thinking about it. It's immensely useful and flexible. We can build better type systems than are in common use. So much more is possible than just making sure we don't stick an int where a string is supposed to go. Moving forward is about raising the bar on what we get "for free". We have a lot of experience building programs that help us program (e.g. compilers, IDEs, build systems) We can move forward without falling into traps (low performance, high programmer knowledge required, overly rigid, more work required than gained in productivity) There are no silver bullets but we can continue to improve.