What is meta? ×
Meta Stack Exchange is where users like you discuss bugs, features, and support issues that affect the software powering all 130 Stack Exchange communities.

This question was closed as off topic:

What is an idiomatic style to do an Isabelle proof by cases?

Some have said now that "off topic" was not the right choice for closure, but with it's x minutes of fame, the question is now being rejected on other grounds.

I'm not going to edit the question to try and make it more acceptable, but I try to counter the claim that this question has very little or no real substance to it, the question being, "Is there a way of making this more readable?"

Below, I provide primary and secondary evidence to support my case. The primary evidence will be the PhD dissertation of Makarius Wenzel, who is one of the three principal developers of Isabelle, and who I have no affiliation with.

The secondary evidence is my own use of Isabelle, and the importance to me that Isar can be tweaked to be more readable than most programming languages. At the bottom, I will include an image showing a little bit of Isar as I've used it.

Isar - readability was on Wenzel's mind a long time ago

Wenzel's dissertation was published about 2002, and the link is here:

http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html

By doing more than mentioning the title of his dissertation, I'm probably belaboring the point. The document title is Isabelle/Isar - a versatile environment for human-readable formal proof documents.

"Isar" is actually an acronym, and it means "Intelligible semi-automated reasoning", where it appears that "intelligible" is a synonym for "human-readable".

A little context

It might help to know some of the history of Isabelle to understand where Isar fits into the scheme of things.

Larry Paulson graduated from CalTech with a B.S. in math, then received a PhD in computer science from Stanford, where afterwards, at Cambridge, he extended the work of Robert Milner and Mike Gordon by developing a generic "proof machine" called Isabelle/Pure (From LCF to HOL: A Shorty History, by Mike Gordon).

Tobias Nipkow from TUM then got involved and was instrumental in developing a logic called Isabelle/HOL on top of Isabelle/Pure. Isabelle/HOL has gained a relatively big following, since it caters more to the programming crowd, where Paulson's Isabelle/ZF never caught on much. Wenzel then got his PhD under Nipkow at TUM, where he put the high-level language Isar on top of Isabelle/Pure.

The three developers are still actively developing Isabelle, along with lots of other developers around the world. If you were to call them all software gurus, they would feign modesty and tell you that you're mistaken.

Structured proofs, did I forget to mention that?

There is the graphical syntax of Isar, but readability is, even more probably, heavily tied into the fact that Isar facilitates structured proofs. A structured proof is a forward proof which is geared more to how humans think. Basically, it's a series of implications,

A ==> B ==> ... ==> Q, therefore, A ==> Q.

Please correct me if I'm wrong.

I gave the short history lesson so I could tie it into my point here about structured proofs. This thing about readability being a big part of Isabelle isn't an accident. The principal developers and their legions made it happen. The older code from the 1980's is based on tactics rather than structured proofs, and it's heavy in ML rather than Isar.

Do I sound like I'm an authority on all this? I'm not.

Me and my preferences

I'm gone on too long, but I wouldn't be using Isabelle as a product if it didn't have features which allow me to produce code that is somewhat meant to be read, rather being like normal code, which is only read if necessary.

I include an image below. It's of a very simple, structured proof. If you think that's the way everyone does things, you would be thinking wrong. If you look at the source code for Isabelle/HOL, which is on the Web, they didn't concern themselves with making it extraordinarily readable. Even with an essay, you have to work to make it readable.

If the code in my image doesn't look like any coding is really being done, it's because the automatic proof methods, such as simp and metis hide most of it.

Also, Isabelle is not all sugar coated candy for coding wimps, there's ML to be used, which has syntax which isn't nearly as nice as Haskell, though they're both functional programming languages.

When you close questions like the OP's, you potentially deprive me of an easy lesson

The learning curve for Isabelle is huge. With Isabelle, you have at your disposal detailed proofs, then automatic proof methods, like simp and metis, and then automatic theorem provers, which Sledgehammer uses to find metis proofs.

I have a need to learn how to do detailed, structured proofs, but the power of the automated methods keeps me going, so I learn a little here and there about structured proofs, which ultimately is all tied into natural deduction logic, which ends up being one more thing on the learning curve.

Simply put, the simple code template that the OP used was instructive to me.

The slight variation he gave as his own answer will be useful to me. I could have already worked through numerous Isabelle manuals and tutorials, yet not have seen Isar syntax used in that way. It's like Perl, there's lots of ways to do things

Did he ask a good question? It was good enough for me. If he wouldn't have asked the question, he wouldn't have given the answer, and it will be a very useful tip.

People can edit this for brevity if that's what's needed.

Some links

Most people will not be familiar with Isabelle as language, so here are a few links. It's a great product.

  • Isabelle is a language/platform that is primarily categorized as a a proof assistant, another major proof assistant being Coq.
    • [Isabelle web site] isabelle.in.tum.de.
    • [Isabelle wiki] en.wikipedia.org/wiki/Isabelle_(proof_assistant)
    • [Coq web site] coq.inria.fr
  • There is Isabelle/Isar as the proof language, and Isabelle/HOL as the programming language.
    • [Isabelle/HOL web page] isabelle.in.tum.de/dist/library/HOL/index.html
  • The foundation for Isabelle/HOL is Isabelle/Pure and Isabelle/ML.
  • The cornerstone of everything is ML, a functional programming language that preceded and influenced Haskell as a functional programming language.
    • [ML wiki page] en.wikipedia.org/wiki/ML_(programming_language)

The image

share|improve this question

closed as off-topic by Martijn Pieters, rene, Gilles, Rory Alsop, Lance Roberts Jun 20 at 15:27

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "This question pertains only to a specific site in the Stack Exchange Network. Questions on Meta Stack Exchange should pertain to our network or software that drives it as a whole, within the guidelines defined in the help center. You should ask this question on the meta site where your concern originated." – Martijn Pieters, rene, Gilles, Rory Alsop, Lance Roberts
If this question can be reworded to fit the rules in the help center, please edit the question.

11  
It's certainly on-topic for SO, but I don't see how "Is there another way to write this?" is a constructive question. –  animuson May 19 '13 at 14:12
    
It's not that I can't be a picky critique, but as a Isabelle user, I'm not that picky about how people ask questions these days. He's basically asking, "Is there a better way to do this?" Seeing I haven't once done a proof by cases yet, I'm just happy to get exposed to a few pointers here and there. Also, I would disagree with you. Readability of proof code is huge with people like me. The goal is a natural language style. Downvotes. It's such a game here. Self respect is more important than some upvotes. –  user222780 May 19 '13 at 14:23
12  
Off-topic might indeed be a bit of a stretch, but "Is there a way of making this more readable?" does not make a good question. The whole "these close voting users don't use Isabelle" line does not mean much. I am unclear on whether readability might be more of a Code Review topic, but I would have voted to close it on SO as well. –  Bart May 19 '13 at 14:24
    
It is a nice feature of SO that any user can ensure the content is high quality. This way the Isabelle users do not have to suffer from rot due to inactivity of a small group. –  user7116 May 19 '13 at 14:35
    
I'll make this my last comment about this (after another one to the answer below, or maybe more). @sixlettervariables, you deal with the problem at hand, and at this point, the problem is not rot. I care about the info I got from the question. Anyone who doesn't know the language can't even know the significance of the question. If it was too conversational and included too much personal info, then it just needed to be edited. –  user222780 May 19 '13 at 14:48
9  
@GC44 If there is anything to "readability" that has a definition, implied constraints, or significance for Isabelle beyond that of what we would normally consider it to be, then make sure to clearly outline this in the question. It might certainly help improve the situation. Whether it will resolve the problems though, I'm not sure. And note that this is not an attack on Isabelle. You seem to take it as one. There is no need to defend Isabelle itself. This is all about the question asked. –  Bart May 19 '13 at 14:52
    
@Bart, thanks for your time. There is a need to defend in sense of informing people, "Hey, this Isabelle thing you've never heard of does fit under the broad category of programming, and recently, the Isa developers decided that SO is the best site to get Isabelle going on Stackexchange." I didn't really ask a question. I made a complaint. It wouldn't get reopened anyway, so there's not much incentive to ask the perfect meta question. The crowd rules; it sticks together. Of course, I'd hate for the other Isa users to suffer because of me. Oh well. –  user222780 May 19 '13 at 15:52
2  
@GC44 You're right, if you have no desire to put any effort into improving the question to see it reopened, it's not going to be. Then again, if all you want to do is complain, Meta will not be a welcoming place for you. If you however want to understand, discuss, or constructively find a solution to the issue, you're more than welcome. This is not about crowd rules, or some sort of oppression of Isa users. Want that minor community to get the most out of their experience? Then do your best to improve the content and ask us for advice on how to do so. We'll gladly help any constructive user. –  Bart May 19 '13 at 15:58
6  
@GC44 I admit that I haven't even heard of Isabelle before, so I'd be interested in hearing what makes the "Is there a way of making this more readable?" question more appropriate for Isabelle than for other programming languages. I mean, if someone asked the same question about any other language the question would be closed as well. Is there something about Isabelle that makes code readability more relevant? –  Juhana May 19 '13 at 16:12
    
@Juhana, thanks for the interest. I'm an imperfect IsaEvangelist. For your question, and to address the Bart's counterpoint below, I need to edit my meta question, if that's tolerable to people. It'll be a number of hours before I do that. –  user222780 May 19 '13 at 17:05
    
@Juhana, it's up. I tell you because you asked. It doesn't look like my edit has gained me any points on the SO ladder of life. –  user222780 May 20 '13 at 0:47
4  
I'm sorry, but your updates don't change my point of view. That "Isar can be tweaked to be more readable than most programming languages" and that readability was a great concern in the technology's development does not mean that asking "how can I make this more readable" within that same technology is a good question. It doesn't make it any less subjective. Furthermore, you liking or valuing certain content doesn't make it any less of a candidate for closure. There are several excellent resources on the site I would hate to see go. But I agree with them being closed because it should be. –  Bart May 20 '13 at 7:38
2  
I'm afraid I don't understand how the vast majority of your edit is relevant to the question at hand. The history and/or usefulness of a language, while interesting, has no bearing on whether a question is good or not. –  ben is uǝq backwards May 20 '13 at 11:58
4  
@benisuǝqbackwards It seems the OP think we're attacking and dismissing Isabelle altogether. And that we're against the building of a topic-related community on SO. Which I think would explain his defence of the topic as a whole, using the history to legitimize it. But all that would be based on the wrong assumption that we have any problem with the topic. It's purely the single question that is problematic. –  Bart May 20 '13 at 12:01
1  
@GC44 "off-topic" was a majority decision, but not necessarily the decision of all users. Others might have voted to close for different reasons. Those don't appear in that case. –  Bart May 20 '13 at 17:05

3 Answers 3

To me this is once again a self-answer trap a lot of users seem to step into. As the user states at the end of his question:

(In case you are wondering about this contrived conversation with myself: This is one of the things that Makarius taught me when he gave me an Isabelle crash course in the course of our collaboration leading to this comparison of different theorem provers applied to auction theory. Posting these lessons here is our way of sharing them with the rest of the world.)

Sharing your knowledge with the world is admirable. And if you can share great, on-topic questions and answers with the rest of the world, by all means do so. And that is often where things go off-track. The content contributed might not be all that bad, but it doesn't make for a good question-answer pair within the boundaries of Stack Overflow. In this case the question boils down to the single line

Is there a way of making this more readable?

And that is not a great question. I would personally not go for an off-topic closure. "Not constructive", or perhaps even "too localized" would have been better fits in my opinion. Because what does "more readable" mean? Readability seems to be a rather personal concept. There might be many answers, one not necessarily more correct than the other. A matter of opinion if you will.

I commented this before: If there is anything to "readability" that has a definition, implied constraints, or significance for Isabelle beyond that of what we would normally consider it to be, then make sure to clearly outline this in the question. It might certainly help improve the situation. Whether it will resolve the problems though, I'm not sure.

Does that mean the content is bad? No, not necessarily. It's just not for Stack Overflow. The whole "rant" against users closing content they are not familiar with is not really justified in most cases. It is often easy enough to evaluate what is being asked and what kind of answers are invited as a result, to be able to judge the question without expert knowledge in the intricacies of a subject. While I somewhat understand you're upset about a favourite topic getting such a treatment, I think it's in line with site policy.

Taking all that into account I feel the closure was appropriate.

share|improve this answer
    
It isn't the worst self-answer, certainly not the best either. These stylistic questions are definitely a gray area. –  user7116 May 19 '13 at 14:46
    
@sixlettervariables Oh no, not at all. It's not dreadful. I just don't think SO is the platform. –  Bart May 19 '13 at 14:48
    
@Bart, with Isa and SO I'm a nobody. As a somebody, you might know a better SE site for Isabelle. The difference in codes given aren't trivially unimportant. The "Is there a better way?" is a legitimate question format. You didn't completely address what it means that they chose "off topic" for closing. It means they didn't understand the subject at hand, and extraneous verbiage and imperfect style wasn't the issue; that could have been edited. That it's closed, oh well; it's answered. I'm still learning from it. It's implicit vs. explicit. Like Perl, there's lots of ways to do things. –  user222780 May 19 '13 at 15:28
    
"It means they didn't understand the subject at hand" ... that is entirely your reading of their motivation and not necessarily what happened. In fact, I don't think that's what the problem was, as I have outlined. You thereby completely glance over and dismiss my explanation. Your opinion, fair enough, you don't have to agree. that said, if it could have been edited to improve it, do so. The question is closed, not deleted. If you can make it a good question it can be reopened. –  Bart May 19 '13 at 15:54
2  
@GC44: Actually "is there a better way?" is not a legitimate question. There always is a better way, which is why this isn't a great question. You're correct though, that it isn't Off Topic, it is instead Not a Real Question or Not Constructive. Take your pick. –  user7116 May 19 '13 at 16:45
    
@Bart, thanks for the offer. You're a better mannered man than me. I suppose I'll edit his question, but it's not my question, and I don't like the idea of messing with other people's words, especially if it's in vain. The answer to a question many times is what defines the value of a question. For this question, it might be hard to demonstrate the value without comparing the slight changes he made to the code in the answer. To address your main point about "readability" and its relation to Isabelle/Isar, I'll have to edit my meta question. Right now, I have to go somewhere. Thanks again. –  user222780 May 19 '13 at 17:01
    
@GC44 If you don't feel up to the task, don't worry. I see you have linked to this particular discussion. If the OP comes here and feels he can make it a better question, perhaps he can do so. –  Bart May 19 '13 at 17:02
    
@Bart, thanks for your elaborate explanation of why SO might not be the right platform. This is quite instructive for me as a newbie. Honestly I wouldn't have expected such a traffic to be generated by my naive Q&A post. In any case, I'll finish reading all comments on this page, and then see whether I can edit my question, e.g. define "readability" more precisely. Or otherwise – well, what would I do otherwise? Delete the question, or will it be auto-deleted after a while, i.e. am I expected to do something? –  Christoph Lange May 22 '13 at 23:34
    
@user222780, I wouldn't generally mind you editing my questions. If I do mind I will complain in every individual case ;-) –  Christoph Lange May 22 '13 at 23:35

This thing about readability being a big part of Isabelle isn't an accident.

Whether it's a big part of the language or not, readability is ultimately subjective. If there is no objective standard to work from to define what is more "readable" and what is less, then there's no way for anyone to answer that question outside of their own personal preferences. And if there is such a standard, any question asking about readability should cite this standard (unless it's commonly used enough among language users that it's generally assumed).

Did he ask a good question? It was good enough for me.

That is not an appropriate standard for whether a question remains open or closed. We don't allow subjective questions here, even if they could be useful to you or others.

share|improve this answer

The question has been closed, not deleted. As such the information in it is still available to you and any other Isabelle coder who comes by it. The contributions have not been lost or wasted.

I wouldn't have voted to close this question myself I have to say - but the point I want to make is that whether the close voters are Isabelle coders or not is irrelevant. They are qualified to cast a close vote by virtue of the fact they have 3000+ rep. End of story.

You don't have to prove your abilities in a certain tag in order to decide whether or not a question is valid or not. 3K+ rep means that it has been judged that they have been here long enough to know what the rules are, and what qualifies as a legitimate question.

share|improve this answer
1  
3K+ rep means that it has been judged that they have been here long enough to know what the rules are, and what qualifies as a legitimate question. Quite sure most of the cases are due to this effect: davidwees.com/content/5-little-monkeys. Most people on SO are not active on Meta. –  nhahtdh May 20 '13 at 3:34
    
@nhahtdh - haha, yes exactly. 3K means you've been around long enough to know better than to go for the bananas! –  McNab May 20 '13 at 7:26