Whiley Talk at Wellington JUG (VIDEO)

Last month, the Wellington Java User Group was kind enough to invite me to give a talk on Whiley.  The talk is a general introduction to Whiley, including the syntax, some issues related to implementation and inter-operation with Java.  The talk was video and, finally, after some faffing around I’ve uploaded it onto YouTube here:

Anyway, enjoy!

UPDATE: Thanks to Evan for suggesting upload the slides as well — you can get them here!

4 comments to Whiley Talk at Wellington JUG (VIDEO)

  • Evan Shaw

    Are the slides available anywhere? They’re difficult to read in the video.

  • Hey Evan,

    Good idea! I’ve put a PDF version of the slides now.



  • koeniglookup

    You’re probably been told that before, but still: you’re a very good speaker. The video is very enjoyable.

    To the point: page 5 says:
    Pre/Post Conditions and Invariants:
    – Goal is to check at compile time
    – Currently, checked at run time

    I’m pretty sure I’ve seen this before (Spec#?). I’m almost sure I’ve seen this more than once (Cyclone or BitC? Honestly, I don’t remember).
    Still, unless I’m missing something I’ve yet to see this promise being realized. I have a completly unfounded suspicion that there isn’t much we can add to the current type systems to make them even sticter than they are (it seems to me that we hit the complexity wall when we try to do that).
    Hence the question: how far do you think you can extend your constraint propagation system? I really like the goals you’ve set for your language, but aren’t you afraid that at one point you will realize that most of pre/post conditions (especially the non-trivial ones) will have to be checked at run time and there’ll be nothing you can do about it?

  • Hi koeniglookup,

    Thanks! Yes, Spec# is one attempt at this kind of thing. Another good one is the ESC/Java tool. I agree with you that this promise has not been realised properly yet — and that is my goal.

    Yes, fear that I will not be able to make it work is of course a constant. However, I have produced several prototypes now which demonstrate the compile-time verification working to a reasonable degree. In particular, version 0.3.1 probably gives the best demonstration (if you want to run it, let me know as it’s not very user friendly).

    The upshot is that I am pretty confident this thing can be done. Currently, I have spent the last few months rebuilding the automated theorem prover from scratch and I’ve made some excellent progress. I’m hoping the next release (coming soon) will really put this concern to bed …

Leave a Reply




You can use these HTML tags

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>