Sadegh wrote:I could do an exhaustive analysis of everything you've posted here, as well as all of your public Facebook posts (you should lock that shit down buddy),

Sadness. He creepy-likes you more than he creepy-likes me, Thomas.

ScholasticSpastic wrote:

Sadegh wrote:I could do an exhaustive analysis of everything you've posted here, as well as all of your public Facebook posts (you should lock that shit down buddy),

Sadness. He creepy-likes you more than he creepy-likes me, Thomas.

Maybe your Facebook profile isnt lefitst-liberal enough?

Thomas Eshuis wrote:

ScholasticSpastic wrote:

Sadegh wrote:I could do an exhaustive analysis of everything you've posted here, as well as all of your public Facebook posts (you should lock that shit down buddy),

Sadness. He creepy-likes you more than he creepy-likes me, Thomas.

Maybe your Facebook profile isnt lefitst-liberal enough?

Nah. It was, until I deleted it. Too much garbage. I suppose there's a lot of garbage here, but at least I'm not getting it from people I have to see in person, so it feels a lot less personal. Also, there's a lot less Trump-boosting here.

PS: Haskell and purity in programming languages fucking RULES!!!

The fun part, of course, is that avoidance of side effects is considered in practical programming circles to be of immense benefit, with respect to the matter of writing code that works. Because we have a wealth of evidence that unintended side effects generate bugs. It's one of the reasons the object paradigm has taken off, because it seeks to enforce encapsulation in such a manner as to eliminate side effects. If your code is tied explicitly to instances of a specific object, and only affects well defined properties of an object, it becomes far easier to keep track of what the code is doing, because that code will not affect entities other than the objects it is explicitly declared to affect.

I've heard this argument before, but I don't really get it.

Take Java (or Python). Suppose I'm implementing a class that has an instance member that is a contiguous collection (an ArrayList, say). Suppose this collection is a read-only attribute of the class: it should have getter but no setter.

If I care about side-effects and encapsulation, I can't simply have my getter return a reference to the array, because all collections in the standard Java library implement methods which destructively modify them (including a "chuck out all the elements" method!). So if I returned a direct reference and let it go out to some undetermined part of the program, I've no idea if someone is going to call "clear" and wipe out that attribute of my class without my permission. That means instances of my class might be randomly put into inconsistent states by client code. So we're still dealing with the side-effects of mutation in a way that can easily generate bugs. That sucks.

I could return a newly-allocated copy instead, or a deep copy if need be. But that's not nice. For starters, you have to remember to do it! It's also expensive. You might try to avoid the cost by passing out references only to code that you trust and then having another encapsulation boundary to untrusted clients where you do the deep copy, but the challenge of getting that right in the face of future refactors is just another source of bugs. You could instead use an adaptor class which exposes a read-only interface, but come on, these are collections. They're so basic to programming that the standard library should have got them right in the first place.

But standard libraries in OOP rarely do get this right, and this sort of thing pervades OOP languages, even those like Java that were created twenty odd years after OOP was first invented. So as I say, I don't get the argument.

If you take Bloch's, now fairly common, advice in Effective Java, you favour immutability everywhere. And that's certainly one way to avoid (some) side-effects, but it doesn't have much to do with OOP.

VazScep wrote:Use an intel processor? The FPU was verified in HOL Light, and has been for over a decade...

Thank you for this informative post. It resurrected my interest in use of theorem provers and similar tools for formal verification. Following your links led me to the paper describing the FPU verification:

http://www.oocities.org/de/christian_jacobi/publications/bj01_verif_fpu.pdf

(Link is currently down for me; bummer)

I've been working my way through this and it is the first article I've encountered which goes through a concrete implementation of this process, thus serves as a tutorial, and allows me to finally wrap my feeble mind around it.

Since you have extensive knowledge in this arena, could you recommend additional resources of this nature? I've plowed through Wikipedia articles and my eyes just glaze over. Thanks much.

Most non-trivial verifications are at least tens of thousands of lines long (and that's even with automation doing most of the work), and the verification code is generally an order of magnitude longer than the code being verified. You also have to be familiar with the automated tooling, which is often crafted for particular domains, and whole domain specific languages for composing proofs.

So you wouldn't want to look too deep into a big formalisation before starting. It'd be like trying to learn programming via a paper on the Linux kernel source. Even in papers for our own community, we gloss over most of the detail that goes into our verifications.

But if you're interested in a tutorial which starts from simple examples, there's a recent and very up-to-date book available as HTML here. It does assume a bit of familiarity with Haskell or ML (you at least should know about lambdas and algebraic datatypes).

If you have access to a university library or are willing to fork out a hundred quid, there's the Handbook of Practical Logic and Automated Reasoning, which takes you from scratch through building a theorem prover with all its assorted automation.

If I could get an idea of your background, I might be able to find some other stuff. I'd been thinking about writing my own tutorial starting from a toy logic, as an introduction to logic itself. Until then, I'm more than happy to write posts here if you have questions.

VazScep wrote:Most non-trivial verifications are at least tens of thousands of lines long (and that's even with automation doing most of the work), and the verification code is generally an order of magnitude longer than the code being verified. You also have to be familiar with the automated tooling, which is often crafted for particular domains, and whole domain specific languages for composing proofs.

I've got a fair bit of work ahead of me.

But if you're interested in a tutorial which starts from simple examples, there's a recent and very up-to-date book available as HTML here. It does assume a bit of familiarity with Haskell or ML (you at least should know about lambdas and algebraic datatypes).

I've only had a chance to glance it over but it looks fine.

If you have access to a university library or are willing to fork out a hundred quid, there's the Handbook of Practical Logic and Automated Reasoning, which takes you from scratch through building a theorem prover with all its assorted automation.

That really sounds excellent. Money is less of an issue than time, at least these days.

If I could get an idea of your background, I might be able to find some other stuff.

Education physics, vocation is about 30 years of application programming. C, C++, C# as primary languages, Ruby for fun, but always like to look at languages just for their own sake.

I'd been thinking about writing my own tutorial starting from a toy logic, as an introduction to logic itself. Until then, I'm more than happy to write posts here if you have questions.

When you have a tutorial, I'd sure like to read it. In the meantime, I will ask questions if something is pressing, but I don't wish to squander your time.

Thanks again.

Kat Dorman wrote:

VazScep wrote:Most non-trivial verifications are at least tens of thousands of lines long (and that's even with automation doing most of the work), and the verification code is generally an order of magnitude longer than the code being verified. You also have to be familiar with the automated tooling, which is often crafted for particular domains, and whole domain specific languages for composing proofs.

I've got a fair bit of work ahead of me.

I didn't mean to make it sound daunting! But it's like learning a whole new programming language. Your starting aim probably isn't going to be to complete a real world project. You'd start by just having fun and enjoying the feedback from the computer, even if doing toy examples.

Some of us are looking towards building verifiers that aim to do everything for you: all you do is break the problem down into logical formulas that are the intermediate results, and get automation to connect the dots. Not sure how feasible that's going to be, but if it works, it'll give theorem proving a very low barrier to entry.

Education physics, vocation is about 30 years of application programming. C, C++, C# as primary languages, Ruby for fun, but always like to look at languages just for their own sake.

Cool. The Handbook of Practical Logic might be okay. He introduces ML, the syntax of which you probably won't find very familiar, but the semantics should be graspable. With the subset of ML he uses, it should be possible to copy and paste the whole lot into F# and have it run.

When you have a tutorial, I'd sure like to read it. In the meantime, I will ask questions if something is pressing, but I don't wish to squander your time.

Ha! Don't worry about that. I'm on this forum to do precisely that, and one of my favourite threads was this one where I got to talk about formal logic and programming for eight pages or so.

VazScep wrote: Your starting aim probably isn't going to be to complete a real world project.

Definitely not. It would be nice if it eventually leads to that, but I won't lose sleep if it doesn't. Just gaining the understanding will be satisfaction enough.

Some of us are looking towards building verifiers that aim to do everything for you: all you do is break the problem down into logical formulas that are the intermediate results, and get automation to connect the dots. Not sure how feasible that's going to be, but if it works, it'll give theorem proving a very low barrier to entry.

Sounds awesome. Maybe by the time I've learned the nuts and bolts, I won't have to.

He introduces ML, the syntax of which you probably won't find very familiar, but the semantics should be graspable. With the subset of ML he uses, it should be possible to copy and paste the whole lot into F# and have it run.

Ocaml was one of the languages I examined briefly, but it's been quite awhile and it was at the bar killing time until others showed up, typically. Not the best scenario for retention. I'll take it more seriously this time.

I've been working one contract for 14 and a half years. It's coming to a close at the end of this month. Naturally, they're squeezing every last drop from me, I barely have time to scratch my ass. But then I'll have two months of freedom where I can really dig in. After that, back to the grind.

In other news, Prayar Gopalakrishnan wants a machine to detect Perl programmers.