5 ms·

Whiley, a programming language with extended static checking

39 points by stefano 15y ago

wccrawford 15y ago
So for non-trivial validations, how does it do? I mean, "requires y != 0:" is really simple. I'm guessing that for more complex things ('name' field of record does not already exist in the database) that you'll have to program them the old-fashioned way anyhow. Which leaves you code a mix of the 2 ways. And really, wouldn't this be just as good and concise? throw "Y can't be zero" if y == 0
- andrewflnr 15y ago
  The point of a requires clause (as I understand it) is to have it be verified at runtime (edit: I mean compile time). You lose that if you do it as an exception. "just as good" is debatable, but it's definitely not equivalent.
  - wccrawford 15y ago
    Yes, I'd forgotten that bit already... But I don't know how you can check that without running it for anything but the most trivial programs.
    - andrewflnr 15y ago
      Oops. Fixed. There is a fair bit of theory about static verification/analysis of programs, a lot of which is applied in optimizing compilers as well. I'm not familiar with it, but I imagine that in this case it just fails on anything less than positive proof, and is comfortable with the strict standard that imposes. It talks more about constraints here: http://whiley.org/guide/constraints/ http://whiley.org/guide/constraints/ .
    - fmap 15y ago
      You are right, the problem is undecidable in general. If the compiler is unsure whether a constraint is satisfied it will have to add a runtime check. This is similar to the behavior of array accesses in Java: If you access an invalid index the JVM is required to throw an out of bounds exception. In practice this would be unacceptably slow and if the compiler can prove that such an exception can never happen, the check will be removed. As for the "simple" example of testing "y == 0", this is actually already undecidable. If you are interested, you might have a look at Nielson's "Principles of Program Analysis", I think that this particular example (undecidability of MOP Constant Propagation) is worked out there. Also, the book is a nice introduction to the subject.
      - redjamjar 15y ago
        The good news about undecidability is that, for the most part, it's not a problem. That is, the problem instances that arise in practice are almost never actually undecidable.
  - bokchoi 15y ago
    No, the requires clause is verified at compile time. To successfully compile, you must perform a check (y != 0) before calling the f function. The compiler verifies that y will never be zero when called.
andrewflnr 15y ago
As primarily a Python programmer with some C++ in my background, Whiley is a fascinating mixture of the familiar and the unfamiliar. The indentation-based blocks are from Python, the function type syntax is like C++, among other ways I would feel at home. But then it throws in ~= as an instanceof operator, and has weird (for me) mutability and object models. Altogether, just having read a lot of the language guide, I could see myself programming something in it tomorrow, given some more research.
- redjamjar 15y ago
  Hey, So, what do you think would be better than "~="? (that's a genuine question since the syntax is not locked down yet by any means). I thought about "isa", also "<:" (following academic papers) and, of course, plain old "instanceof". But, the latter is too much finger typing for me ... Oh, and of course we could do something like "typeof(x) == int" etc
  - andrewflnr 15y ago
    Off the top of my head, a simple "is" would be nice. Pronounceable and short.
    - munificent 15y ago
      It's what C# uses too. Seems to work well.
      - redjamjar 15y ago
        ahh, that's interesting I didn't realise that!!
  - kiwidrew 15y ago
    I rather like how Go decided to handle this, using "type switches": switch x := node.(type) { case Node: // x is of type Node in this block case Leaf: // x is of type Leaf in this block } (http://golang.org/doc/go_spec.html#Type_switches http://golang.org/doc/go_spec.html#Type_switches)
jules 15y ago
Link to Extended Static Checking for Java paper not behind a paywall: http://www.eecs.umich.edu/~bchandra/courses/papers/Flanagan_ESC.pdf http://www.eecs.umich.edu/~bchandra/courses/papers/Flanagan_...

39 points by stefano 15y ago

So for non-trivial validations, how does it do? I mean, "requires y != 0:" is really simple. I'm guessing that for more complex things ('name' field of record does not already exist in the database) that you'll have to program them the old-fashioned way anyhow. Which leaves you code a mix of the 2 ways. And really, wouldn't this be just as good and concise? throw "Y can't be zero" if y == 0

andrewflnr 15y ago
The point of a requires clause (as I understand it) is to have it be verified at runtime (edit: I mean compile time). You lose that if you do it as an exception. "just as good" is debatable, but it's definitely not equivalent.
- wccrawford 15y ago
  Yes, I'd forgotten that bit already... But I don't know how you can check that without running it for anything but the most trivial programs.
  - andrewflnr 15y ago
    Oops. Fixed. There is a fair bit of theory about static verification/analysis of programs, a lot of which is applied in optimizing compilers as well. I'm not familiar with it, but I imagine that in this case it just fails on anything less than positive proof, and is comfortable with the strict standard that imposes. It talks more about constraints here: http://whiley.org/guide/constraints/ http://whiley.org/guide/constraints/ .
  - fmap 15y ago
    You are right, the problem is undecidable in general. If the compiler is unsure whether a constraint is satisfied it will have to add a runtime check. This is similar to the behavior of array accesses in Java: If you access an invalid index the JVM is required to throw an out of bounds exception. In practice this would be unacceptably slow and if the compiler can prove that such an exception can never happen, the check will be removed. As for the "simple" example of testing "y == 0", this is actually already undecidable. If you are interested, you might have a look at Nielson's "Principles of Program Analysis", I think that this particular example (undecidability of MOP Constant Propagation) is worked out there. Also, the book is a nice introduction to the subject.
    - redjamjar 15y ago
      The good news about undecidability is that, for the most part, it's not a problem. That is, the problem instances that arise in practice are almost never actually undecidable.
- bokchoi 15y ago
  No, the requires clause is verified at compile time. To successfully compile, you must perform a check (y != 0) before calling the f function. The compiler verifies that y will never be zero when called.

andrewflnr 15y ago

As primarily a Python programmer with some C++ in my background, Whiley is a fascinating mixture of the familiar and the unfamiliar. The indentation-based blocks are from Python, the function type syntax is like C++, among other ways I would feel at home. But then it throws in ~= as an instanceof operator, and has weird (for me) mutability and object models. Altogether, just having read a lot of the language guide, I could see myself programming something in it tomorrow, given some more research.

redjamjar 15y ago
Hey, So, what do you think would be better than "~="? (that's a genuine question since the syntax is not locked down yet by any means). I thought about "isa", also "<:" (following academic papers) and, of course, plain old "instanceof". But, the latter is too much finger typing for me ... Oh, and of course we could do something like "typeof(x) == int" etc
- andrewflnr 15y ago
  Off the top of my head, a simple "is" would be nice. Pronounceable and short.
  - munificent 15y ago
    It's what C# uses too. Seems to work well.
    - redjamjar 15y ago
      ahh, that's interesting I didn't realise that!!
- kiwidrew 15y ago
  I rather like how Go decided to handle this, using "type switches": switch x := node.(type) { case Node: // x is of type Node in this block case Leaf: // x is of type Leaf in this block } (http://golang.org/doc/go_spec.html#Type_switches http://golang.org/doc/go_spec.html#Type_switches)

jules 15y ago

Link to Extended Static Checking for Java paper not behind a paywall: http://www.eecs.umich.edu/~bchandra/courses/papers/Flanagan_ESC.pdf http://www.eecs.umich.edu/~bchandra/courses/papers/Flanagan_...