8 ms·
The example given with the `Point` struct is interesting. As a self taught developer with admittedly little language design knowledge, it almost seems like unit
by scriptkiddy 7y ago
The example given with the `Point` struct is interesting. As a self taught developer with admittedly little language design knowledge, it almost seems like unit tests without all of the boiler plate.
For instance, the `is_diagonal` function provided as the "correctness checker" looks to me like something that would be in a unit test for the `double` function. However, I think it goes a little bit deeper than that. In a unit test, you are somewhat required to pass specific values to the constructs you are testing. The given example is more complete than a unit test in that it doesn't just test for the correct value being produced by the `double` function when given specific values, it actually checks all possible outcomes by asserting that the `double` function always produces a `Point` where `p.x == p.y`.
Given that the example is relatively trivial, I would like to see how this would work for more complex functions and structures.
- pjc50 7y agoThere is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones.
- seanwilson 7y ago> There is a lot to be said for understanding types as a kind of test, but performed at development time rather than runtime. And valid for all possible inputs, not just some specific ones. Maybe you know this, but this is a well known correspondence (as in academically from decades ago, but barely mentioned in industry): https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... The types you write in code describe program properties to be proven and the type checker tries to create a proof that those properties are true for all inputs and outputs. Tests as you say only check a small number of inputs/outputs in comparison. It's very similar to mathematics where checking if a conjecture holds for a few values is a poor substitute to a rigorous proof.
- draw_down 7y agoThe insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry.
- seanwilson 7y ago> The insight that proofs and types are analogous is an interesting one, but all of this (the writing, the math, and the code) strikes me as fairly impenetrable. It does not surprise me that this is rarely mentioned in industry. Yes, it does look impenetrable but the high-level idea is fairly intuitive and it's the foundation of many formal proof assistants (e.g. Coq, Idris). I see comments quite often where people suspect some vague links between writing maths proofs and type checking computer programs so I think it's worth knowing a very deep connection has been known about this and researched for decades.
- giornogiovanna 7y agoThe simplest place to start, in my opinion, is [0]. If you understand that, then the fact that types are propositions and proofs are values of those types seems pretty obvious. [0]: https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%...
- aassddffasdf 7y agoProperty-based tests do this at runtime too (and they catch far more bugs than you'd imagine going into it).
- seanwilson 7y agoProperty-based tests are really practical and will find bugs unit tests don't, but type checking is an exhaustive proof that the properties you've expressed with types hold for all inputs/outputs. A key point though is the type systems of most mainstream languages don't let you express complex program properties (e.g. the input list must be sorted), so your only option is to use unit tests or similar to check those.
- enqk 7y agoThis understanding shows also the flexibility that unit tests brings to the development cycle: contrary to type checks, they can be temporarily disabled so as to shorten the iteration loop when necessary, and re-enabled after adjustments have been made. (Contrast with long compile times which are incompressible)
- _Codemonkeyism 7y agoSomething in between what you describe and what the article does with F* would be Haskell QuickCheck or Scala ScalaCheck [1] testing where the framework determines the test parameters for your tests. [1] https://www.scalacheck.org/ https://www.scalacheck.org/
- ChrisSD 7y agoDoes the linked case study[0] help at all? It's real code that already had debug assertions that acted as a postcondition. It was than formally proved that those conditions held (or didn't hold in one case) for all the relevant functions. [0] https://blog.merigoux.ovh/en/2019/04/16/textinput.html https://blog.merigoux.ovh/en/2019/04/16/textinput.html
- scriptkiddy 7y agoIt does help. what I find interesting here is that the prover was able to find a potential bug that the test cases were not able to find. That's powerful.
- rotcev 7y agoYou might be interested in clojure.spec [1] too :) [1] https://clojure.org/guides/spec https://clojure.org/guides/spec
- max76 7y agoThe rust compiler will help you avoid a lot of common runtime errors. It comes at a cost of extra development time. The Rust philosophy values code correctness over developer efficiency.
- im_down_w_otp 7y agoI'm confused by this sentiment. How efficient is a developer when producing things that are incorrect? Unless the goal is produce incorrect things, which seems unlikely. It seems like the philosophy prefers knowing ahead of time what's wrong over discovering it incidentally, and probably accidentally, after the fact.
- swsieber 7y agoThere are many times where you don't need 100% correctness (e.g. prototypes, or edge cases that in practice are never hit) - I'd say it might be more accurate to say that Rust makes it harder/less convenient to take out technical debt. I discovered a bug that could potentially be triggered in the codebase where I work, but never has. It's about 5 years old. You don't actually always need technically correct - sometimes you want practically correct, where "practically" covers a huge spectrum.
- melling 7y agoI think we're talking about typing time, right? Because if say, 75% of your time is spent debugging in an "regular" language then you really aren't saving much time by reducing the amount of code you must write. If we could reduce programming to typing in mostly correct code then software development will be much faster, even if the code we type is 50% longer.
- int_19h 7y agoLook up "design by contract" for more background on these. I really hope this will be the next mainstream thing in programming language design, after the current functional wave. Even without fully perfected static analysis tools, just the dynamic checks alone are well worth the trouble of writing good contracts, IMO. They also make for better, more precise documentation.
- nemlog 7y agoDesign by Contract (DbC) was seamlessly embedded into the Eiffel Language and Method right from the start, way back in 1986. The ideas gained by using Eiffel and Design by Contract can be formative and help us in our approach to using other languages. The foundational ideas around DbC and Eiffel for requirements and their proof still evolve and progress 33 years later with AutoReq. A paper describing AutoReq was recently published .. AutoReq: Expressing and verifying requirements for control systems https://www.sciencedirect.com/science/article/pii/S1045926X18301514?dgcid=author https://www.sciencedirect.com/science/article/pii/S1045926X1...