On 4/16/10, Bernhard Brodowsky <brodowsb / student.ethz.ch> wrote:
> Caleb Clausen wrote:
>> On 4/15/10, Bernhard Brodowsky <brodowsb / student.ethz.ch> wrote:
>>> Hi, I want to try to prove some parts of my programs formally. Does
>>> anyone have any experience with the combination of formal methods and
>>> Ruby?
>>
>> I don't know much about formal methods, but my guess is that it is
>> very, very difficult to formally prove a ruby program. Most types of
>> analysis of ruby code are somewhere between very hard and actually
>> impossible due to the very dynamic nature of ruby. It's because you
>> can change so much of the behavior of the language at runtime, so you
>> can't tell until you actually are running a particular bit of code
>> what it might do.
>
> It is most certainly true, that it is extremely difficult, but one has
> to be ambitious some times. And actually, my formal methods professor
> told me that it was difficult, but not impossible, but it depends which
> properties I wanted to prove. Things like that I never call a method on
> "nil" could be possible to prove according to him, so I just want to
> give it a try.

It should be fairly easy to prove that kind of thing in some special
cases, but the general case gets hairy.

I agree that's it's not (quite) impossible, but.... you're definitely
headed into untrod territory. Keep me (and the list) informed of your
progress, since this would be very cool if you succeed.

PS: if you do succeed, your professor better give you a phd. No,
seriously. It's that hard.