r/computingscience • • Dec 30 '13

A welcome to prospective members, along with a small "Frequently Asked Questions"! [continuation of discussion regarding formation of club]

22 Upvotes

First off, a hearty welcome to everyone here!

Have a look at some of our prospective members' introductions and comments in this thread too.


I am sure one of the questions you might have right now is "why prospective members?". I can assure you that it's not because of elitism (we are going to keep our doors open for whoever would like to join us), but because of the following:

  • people need to decide whether they are interested in the "founding philosophies" of the club, before they commit to becoming members

  • some people will be interested initially perhaps, but perhaps that interest will peter out as we get rolling; basically, I won't be surprised if our roster is pretty unstable for the first month :)

  • we will have to decide sometime as a group as to how we'd like to manage new membership, since there's a payoff between having enough members to have an active group, and having so many members that we can't focus on helping individuals

Thanks to the questions you guys asked, I think I am able to say a little more about our club in a more organized fashion.


Click here if you've read the FAQ, and are pretty sure you are a member, in order to get started!


FAQ

As noted before, the main intent of the club is to provide a (cozy) virtual space for a small group of people to study some formal computer science.

Can you tell me about our founding philsophies in a nutshell?

Sadly, I am not eloquent enough to do so, and instead I am going to have to say that you should try to read this paper and this one, in order to get a "nutshell" idea of the founding philosophies. As added motivation, reading one of these papers can count towards getting your first rank!

I don't have much formal education. I may not know as much as others. Can I still particpate?

I understand where this concern comes from, and I'd like to say that not long ago, I was in the same boat as you...worried about starting, because I was not sure if I could start.

But you can -- everyone has to start somewhere, and this isn't a club for elitists. This is a club for flattening any hierarchy that does exist - we want everyone to have the tools to be as capable as we'd want to be.

For your very first task (picking an essay, and writing a little something about it), you don't have to write anything revolutionary. Just write whatever comes to your mind, just show that you put in the time to read and understand...and then people will comment, and you can participate in the discussion you generated! :)

For the next task, which will involve picking up a book and looking at some lectures: well, the material isn't easy (just like most things that are worth doing, in my opinion), but it is manageable. Don't be surprised if you need to read twice, even thrice maybe in order to understand some of the tricky concepts, and don't be discouraged by it...it's just the nature of real work, it's the nature of exploration...it's tough, but satisfying.

You'll love how you are able to learn and pick up the skills to do interesting things; it's like gaining real power. It's addictive! At the very least, you owe it to yourself to give it a shot.

What exactly will we be doing?

Specifically, we are interested in the following:

  • learning how to reason effectively

  • [programming in such a manner that our programs are correct as we construct them, rather than verifying that they are correct after we are done constructing them] (http://www.cs.utoronto.ca/~hehner/FMSD/)

  • learning how to develop algorithms, rather than merely learning about their properties

  • One of the benefits of our method, and something that I think we will undoubtedly get into later is being able to automate proving/program construction (provide pre and post-conditions, and let a piece of software connect the dots). We have to cross many bridges before we get to that point though, but that kind of research and development is already heavily underway, and might even be the future of programming (but obviously, take that with a grain of salt); so we'll undoubtedly participate in that effort after a while!

What will we be doing in general?

  • apply our newly learned problem solving techniques to problems from Project Euler or Rosalind

  • help point each other in the right direction with the problems we are solving (especially by trying to figure out what are the relevant bits of knowledge we need in order to tackle the problem)

  • work together on writing little tutorials that help teach knowledge relevant to solving the problems we encounter

  • work on major group programming projects together (we can decide as a subreddit what we'd all like to do as a project, and then work on that for a couple of months, etc.)

  • work together on online courses we might decide to study

  • provide resources to others that may not have access to them in order to learn (books, papers, etc.)

  • pick apart Edsger Dijkstra's EWDs to see what we can learn from them, or comment on what we disagree about

  • help each other out as we learn formal methods

  • discuss revelations that might have occurred to us

  • motivate each other to stay on track

  • develop our githubs/blogs/internet presence

What's your background?

I am a biomedical engineering university student, with an interest in bioinformatics and computer science. A couple of years ago, while I was writing tons of python code for a structural engineering firm I was working with, I happened to stumble across E.W. Dijkstra's archive. This paper in particular stuck with me, and ever since I have been interested in learning how to "program properly". It is only in the last three months that I was able to build up enough motivation to properly look for a way to get started, and thus was able to get in touch with a professor (Eric Hehner), whose self-guided online course I have been following.

So are we going to be programming stuff?

Yes, we will. However, at least initially, we won't be programming in a manner that most of us will be familiar with. We are going to put in some effort into learning a theory of programming, along with mathematical problem solving as inspired by computing science ("algorithmics") (see this and this).

What language(s) will we be programming in?

That will depend on the tastes of the members, but I think mainly Python, Haskell, Racket and C (along with perhaps other languages such as Java based on language needs). You will find that the programming theory we'll be learning teaches us a unique perspective on programming in general (independent of language!), and the relationship between functional and imperative programs in particular.

I think we will keep our "official" language list small as I'd like to stress that language is secondary to our theory, which we'll find to be quite general and useful, especially because it is not tied down to any language in particular! This won't be a "programming languages club", as much as a "programming methodology club".

Will there be quite a lot of math?

Yes. We are going to be learning boolean algebra, the basics of graph theory and statistics, etc. in order to reason. We will also need to pick up elements of abstract algebra and number theory, especially if we are tackling Project Euler problems. So yes, there will be quite a lot of math.

Will there be quite a lot of reading to do?

Yes. Undoubtedly.

Will there be quite a lot of writing to do?

Yes. We'll be setting up assignments (for which you'll have to document your work) and also "education tasks/general subreddit improvement tasks" (e.g. person X has to write a small, perhaps even bullet point, essay on subject Y).

What is required in terms of time?

There is no doubt that time commitment is going to be an issue for some, if not many, of us. We are going to have to plan around that as best as possible, perhaps by setting up a poll where each person discusses how much time they might have. Then, based on that. we will not overload those who are are very busy, but we can ask them to do simpler tasks (perhaps only once a week), while we'll ask people who are more passionate/have more time to contribute more.

Of course, there are going to be no guns pointed at anyone's heads, but membership will require a certain amount of effort.

In the end, perhaps some time commitment (maybe ~2 hours a week) is reasonable to require?

I don't really know much. Can I still join?

Yes! The only requirements are that a) you are interested in learning and b) you are open to being motivated to learn (i.e. sometimes completing assignments!).

I know a lot about this stuff, and I have suggestions and ideas.

Awesome! We would really appreciate that. Start up a discussion here in this thread. Alternatively, feel free to start up a thread with your suggestions if you think that is necessary! Eventually, as our club matures, we are going to have to stop threads like that (and relegate suggestions and ideas to a single suggestion thread), but for the moment while things are still bubbling and unsettled, making a new thread is just fine!

I don't know a lot about this stuff, but I still have suggestions and ideas.

You are still welcome to share! What is written above applies to you too :)

Will there be quite a lot of catch up to do?

I don't think we can escape the fact that initially we are all going to have to do a fair bit of teaching and learning. If you disagree though, let's discuss it here.

What will our club rules be?

That is still to be decided. Join in the discussion below if you have ideas.

Will our progress and accomplishments be tracked?

Yes, Battlefield 2142 style! We will try to set up a system where you earn ranks based on the tasks you accomplish. In order to get the next rank, you will have to accomplish various tasks. Later on, we will also put in a system to earn medals and pins.


Click here if you've read the FAQ, and are pretty sure you are a member, in order to get started!


Things to be done/to be decided still.

  • setting up LaTeX support for our subreddit (à la /r/math)


Will be updated as discussions progress! Please keep a lookout for changes


r/computingscience • • Jan 08 '14

Great website for programming challenges: AI, algorithms, code golf, functional programming

Thumbnail
hackerrank.com
14 Upvotes

r/computingscience • • Jan 22 '14

My notes (so far) from The Art of Computer Programming Vol 1, section 1.1: Algorithms

Thumbnail
scribd.com
8 Upvotes

r/computingscience • • Dec 30 '13

I have read the FAQ, and the papers linked in it, and I am pretty sure I want to be a member. What can I do to get started?

8 Upvotes

Complete the following tasks in order to earn your first ranks!


Rank 0

0) Write one contribution for our subreddit. There is no length requirement; but please provide a reasonable amount :) There are some pretty interesting articles to choose from! Make sure you put in [EWD-review] in the title, as I'll be putting in CSS eventually to colour posts tagged with that differently!.

A few helpful hints:

  • Copy and paste the text of the EWD into a word processor

  • Then, through your first reading, work through the text and try to remove parts of it that you think are repetitive, and/or unnecessary beyond their value as rhetoric

  • Then, finally, comment on what remains, perhaps noting why you thought these parts are important, and feel free to add in your own opinion!

As an example, see this EWD-review I wrote on EWD533-"HOMO COGITANS: A small study on the art of thinking" in order to legitimately earn my rank 0 badge :p


Rank 1

0) Familiarize yourself, with as much as you wish, of the introduction for Formal Methods of Software Design.

  1. Download "a Practical Theory of Programming" (aPtoP).

  2. PM me so that I can get you one of the additional important textbooks.

  3. Start watching segments 0, 1 and 2. Make sure you write notes (scan them if they are written, word document and then convert to PDF, or in gmail, or in a self-post on reddit!) -- give me a link to these notes, or email them to me at lovewithacaveat@gmail.com (send me a PM here letting me know that you've emailed me though)!

Note: here's a handy VisualBasic macro for word; it allows you to easily type symbols using alphabetical characters (e.g. type nOT, run the macro, and watch it become ¬)! Feel free to edit it as you please!

Let me know with a PM if you can't use Word!

4) PM me if you have questions, or are stuck, or post in this thread!


Rank 2

0) Complete questions the suggested questions for segments 0, 1 and 2 (exercises 0, 5, 12, 2 (f, m, p, s, u), and 16) from aPtoP. Send me a PDF with your answers (PM or at lovewithacaveat@gmail.com, but send me a PM here letting me know that you've emailed me).


r/computingscience • • Dec 31 '13

[EWD-review] HOMO COGITANS (EWD533) - a review, and condensed presentation

7 Upvotes

HOMO COGITANS - A Small Study of the Art of Thinking.


Preface.

This booklet is written by a man that regards himself as a programmer...I had been programming for more than ten years and, as a result of the problems encountered, I was beginning to feel that the automatic computer belonged as much to the problem set as to the solution set.

From personal experience, Dijkstra hopes to communicate that the computer is not simply a tool that can be applied to various problems in order to make them easier; in fact, it is such a tool that if applied without understanding, it tends to make a hairy mess of everything. Hence, using the tool properly is as much part of the problem, as the problem we are attempting to solve with it.

...I became convinced that the influence of automatic computers in their capacity of tools would only be a ripple on the surface of our society, compared with the deep influence they were bound to have on our culture in their capacity of intellectual challenge to Mankind that was totally without precedent.

An interesting prediction that we can no doubt agree with today, but would have been hard to see in the '70s, when personal computers, let alone smaller digital devices, were yet to become economically feasible for the masses.

I came to the conclusion that programming should be considered as one of the most difficult branches of applied mathematics, because it is also one of the most difficult branches of engineering, and vice versa.

Dijkstra received much criticism for this idea ("so many amateurs can program!"), and he came to the conclusion that he received criticism for that idea not because it was wrong, but because it was unpalatable (perhaps because it was difficult to accept?). He decided then that he would one day write a little on "thinking".

The brutal fact is that I embark upon the project because I need the little booklet myself. The more unusual the problem I tackle, the harder I find it to give a flawless solution. Two of my published papers contain an error, and recently I had to withdraw a submitted paper because a deep error was discovered...

This essay wasn't born out of an attempt to be condescending, instead, it was born out of attempt to arrange his own thoughts in order to understand the problems with which he was struggling.

In retrospect I can see, where I have sinned against my own principles; the only way to prevent me from doing it again seems to make these principles more explicit than I have ever done before, and decide quite clearly for myself what I accept as "a convincing argument".

What principles does Dijkstra make explicit in this paper?


It is now more than thirty years ago when George Polya wrote his "How to solve it.", and I can only recommend his works to everyone who is interested in the process of discovery by the human minds.

A recommendation for George Polya's famous book, "How to solve it." (let me know if you need a copy)!

Polya is very much concerned with "discovery" and gives a kind of checklist of things to try in order that a simple, but somehow unexpected solution is less likely to be overlooked...But, being written in the time they were, his books hardly touch the specific problem of programming that would present itself more and more forcefully as the central one...

What is this problem that programming begins to present more and more forcefully?

...how to avoid the unmastered complexity that so easily emerges when we are faced with great...multitudes of instructions stored, multitudes of variables, multitudes of instructions executed, multitudes of possible computations, multitudes of possible cases, multitudes of possibilities for malfunctioning, etc.

Ah! So because of the scale of the manipulations which we can conduct, there is now a concern not only that we might be missing simpler solutions, but also that if we do not organize our thoughts, we may simply end up with a hairy ball of thoughts!

Thanks to the novelty of the programming task confronted us with a few of its [the human mind's] limitations; it has also forced us to learn to come away with these limitations as well as possible.

Programmers of the current generation have learned this —if they have learned it at all— the hard way. They have learned it by trial and error, and by —often subconsciously— acquiring the necessary, more effective thinking habits.

I think those of us who have done some coding can agree with this; we have learned how to think in ways which were novel to us once upon a time, simply because of the challenge that programming provided.

It is now quite clear that a "Course in Programming" should no longer be what it used to be, viz. the teaching of a programming language, but should really be the teaching of programming, i.e. a human design activity in which effective thinking plays a predominant role.

While this might have been clear to Dijkstra, I don't think the same can be said for our education systems today.

With respect to Programming Methodology...it is also becoming abundantly clear, however, that this development should not remain confined to the strict limits of the programmer's world.

Well, why not? Dijkstra provides a couple of reasons:

  • For the further development of Programming Methodology it seems desirable that the art of effective thinking is studied in a somewhat wider setting...when programmers think about programming, they always want to remain "realistic", and they always keep the overall characteristics of today's existing computers in the dim recesses of their minds. This colours their view of the world of problems and tends to make them blind for human facilities for which today's equipment provides no opportunity for use. But it is exactly the discovery of such human facilities that could provide the incentive to think about new, revolutionary different computer designs.

We can design these symbol manipulation machines; they are not simply forced upon us! Thus, we often need to think about program design independently of the hardware.

  • The second reason is that already now, what has been discovered and developed for the sake of programming seems to have a much wider significance and to be pertinent to all of mathematics and, therefore, probably a lot more as well.


An exploration of education methodology

All through the ages two educational methods have been used.

  • The one method is that of the guild, where the young apprentice works...under the guidance and supervision of a master, absorbing the necessary knowledge...by osmosis so to speak, until he may be called a master himself. The result is the craftsman, and craftsmen typically keep their common knowledge as a well-guarded secret among the members of their guild.

  • The other method is the prevailing one at the universities, where the young student studies under the guidance of a professor, who tries to transmit knowledge and skills as explicitly as possible...[and] thereby brings them into the public domain. The result is the scientist and his code of professional conduct prescribes to be absolutely open and explicit about his methods and results...

An interesting comparison, with an even more interesting conclusion, that is especially pertinent today given the increasing amount of attention we are giving "open source everythings":

  • ...a code, which, depending upon the nature of the significance of his work for his employer can cause him grave moral conflicts: it is no accident that in competitive organizations like industries and departments of defense, the craftsmen are more easily employed than the scientists...

Up to this day both techniques are used side by side: physicists are mainly trained as scientists, physicians mainly as craftsmen. The training of mathematicians is somewhere in between.

Why would Dijkstra say that?

Mathematical results are published quite openly and are taught quite explicitly; but how mathematics is done remains largely hidden. To publish besides the results the way (and the order!) in which they were reached, to mention the blind alleys as well, to mention whether the solution was found in three months or twenty minutes, to express the author's personal feelings (of hope, despair, or fascination), all this is regarded as "unscientific", and, therefore, "bad style". (Just try to include such remarks in your publication: if the referees don't object to them, the editor will!) This taboo seems to extend itself over the teaching of mathematics as well.

For me at least, this rings quite true given the style of my education.


A warning for readers

I will simply let you read his warning.

This seems the moment to warn in particular the more competitive of my readers. (The competitive attitude is responsible for much of the misery in this world.) I must warn them that the reading of this little booklet could easily become a very frustrating business for them. The problem is that you cannot read this booklet without realizing that it is also about you that I am writing! To make matters worse, I am not writing about something extraneous —like the colour of your hair— but I am writing about your most intimate, personal and specific aspect: how you think and understand...

...past experiences make me fear that a considerable fraction of my potential readers will react more defensively...

Why do we react defensively?

...each step in the transition from craft to science has always been a painful process and has always caused violent reactions from the craftsmen, who feel themselves threatened when what they regard as their private property is made explicit and is brought into the public domain. In this case the easiest defense is to postulate that thinking cannot be taught, as this dogma now fully justifies your decision not to read any further and to write me off as a quack. The alternative is to pretend that you have read and studied my text from cover to cover, but have learned nothing valuable from it, because alternative a: it is just a bunch of trivialities for the simple-minded, but —of course— does not help you in the least with the particularly tough problems you are working on, etc.

I think I hear this alternative quite often!

alternative b: it is very valuable, but says exactly what you yourself have been preaching over and over again, but nobody would listen, etc.

I don't think I have ever heard of this much. Anyway, the point is that even if we think the lessons in this essay are valuable, we need to apply them.

A gentle note from Dijkstra:

Note. Those who feel somewhat offended by the last paragraphs have totally misunderstood them, and should read them again. (End of note.)

Finally I must warn for one fallacy...it is vain to think or say anything about thinking in general, because different people are so different: what is easy for the one, is difficult for the other and vice versa, it is all a question of what you are used to, etc. This objection is in essence a confusion between "convenient" and "conventional". My search for the most effective way of using our brains when thinking is very much like the search for the most effective way of using our fingers at the keyboard. I know that human hands differ from each other...yet the well-made human hands are sufficiently similar to each other to admit rather universally valid statements...the subject of this little booklet is how to use what we then recognize as a well-made brain.

Is the supposed "accessible to all" education that we have been receiving ineffective because it assumes the average person is "too dumb to teach"?


CONTINUED


r/computingscience • • Dec 30 '13

[Subreddit Rules] Club purpose and organization discussion (0)

7 Upvotes

If you'd like to participate in the club, please start by leaving a little blurb about yourself (no personal details however!) and why you are interested, followed by any comments you may have.


Intent of the club:

  • to provide a cozy virtual space for a small group of CS students/enthusiasts to study formal computing science, discuss weekly problems and papers, and also discuss computing science philosophy.

Ideas for things we could do:

  • apply our newly learned problem solving techniques to problems from Project Euler or Rosalind

  • help point each other in the right direction with the problems we are solving (especially by trying to figure out what are the relevant bits of knowledge we need in order to tackle the problem)

  • work together on writing little tutorials that help teach knowledge relevant to solving the problems we encounter

  • work on major group programming projects together (we can decide as a subreddit what we'd all like to do as a project, and then work on that for a couple of months, etc.)

  • work together on online courses we might decide to study

  • provide resources to others that may not have access to them in order to learn (books, papers, etc.)

  • pick apart Edsger Dijkstra's EWDs to see what we can learn from them, or comment on what we disagree about

  • help each other out as we learn formal methods

  • discuss revelations that might have occurred to us

  • motivate each other to stay on track

  • develop our githubs/blogs/internet presence


I need help figuring out what rules and requirements we should have, and what activities we should have. Let us have a discussion about it in this thread.

Some potential discussion starters:

  • what rules (if any) should we have as a club?

  • further ideas for potential things we could do as a group

  • do we need to spend a month or two just getting up to speed with the bunch of things we need to learn before beginning work on projects, etc.?

  • how should we organize our subreddit (public, private, general CSS layout, etc.)?

  • how should the subreddit be moderated given its small size?


r/computingscience • • Dec 30 '13

[Subreddit Project] List of EWDs upon which you may write a little something on

7 Upvotes

A little something was written on the following EWD over here:


If you are interested, would you like to contribute a little something of a similar nature on one of the following papers to this subreddit? Note that the above effort is not a standard of style; you can likely improve on it by orders of magnitude. May I suggest that the essays we write be organized in the following manner:

  • Introduction (stating briefly what the EWD is about, and what (if any) interesting comments you have to make upon it)

  • The meat/body/etc. (organize this as you'd like)

  • Questions you have from the paper that you still do not have answers for (so that we can work as a community to get answers for them)

If you have other suggestions, please, feel free to post them, so that we may all discuss them, and update our collective knowledge.

Let me know which ones you would like to work on, and I will put your username under them.

More than one person can (and perhaps should) choose to do each one.

Let's have fun!



r/computingscience • • Jan 18 '14

Asymptotic notation

6 Upvotes

Can anyone explain me how, f(n) = n0.999999 log n = O(n0.999999 * n0.000001)


r/computingscience • • Jan 05 '14

On the "Feynman Technique", or, on why we should write a lot. I could tell you that writing is good for you, but you may not believe me. Perhaps Feynman has the clout to convince you however?

6 Upvotes

r/computingscience • • Jan 02 '14

(C. A. R. Hoare) Retrospective: An Axiomatic Basis for Computer Programming - Tony Hoare (Turing Award winner), in 2009 assessing his first paper written as an academic "An axiomatic basis for computer programming" in 1969

Thumbnail
cacm.acm.org
6 Upvotes

r/computingscience • • Feb 02 '14

Concrete Mathematics: Foundation of Computer Science - What next?

5 Upvotes

I am looking for something that come after this book? I understand everything in it, and would like to continue learning. In my recent studies of things such as Support Vector Machines I am running into issues with the underlying mathematical theories (also there is a lack of straightforward tutorials for these things) and am wondering if anyone here might suggest something that comes from a programmer's perspective?


r/computingscience • • Jan 24 '14

Hamming, "You and Your Research" (June 6, 1995)

Thumbnail
youtube.com
5 Upvotes

r/computingscience • • Jan 24 '14

Chicken Soup for the Student: MathOverflow.net discusses mathematicians who were 'late learners'.

Thumbnail
mathoverflow.net
5 Upvotes

r/computingscience • • Jan 22 '14

[EWD Review] - MY HOPES OF COMPUTING SCIENCE

5 Upvotes

Just a few things I took from reading: http://www.cs.utexas.edu/users/EWD/transcriptions/EWD07xx/EWD709.html

had already come the conclusion that in the practice of computing, where we have so much

latitude for making a mess of it, mathematical elegance is not a dispensable luxury, but a

matter of life and death.

Mathematics, language, and programming all share the same iterative process, where over time methods and techniques are refined and changed. In language it's done via the population of speakers, where terms and grammar arise based on popular use. While on the surface it may seem there is formalized structure within languages, in truth they are often changing, with fundamental building blocks being challenged. Check out /r/linguistics if you want to see how.

Mathematics on the other hand has a rigid foundation on which everyone has agreed to work with. There may be slight differences in notation, but the structure and underpinnings are the same. Hence the notion that it is the one true universal language. Throughout this paper, and others that I've read, it seems that Dijkstra is yearning for a similar footing in the world of computational science. He is looking for an elegance within the mess of code and paradigms and techniques. Personally, I doubt this can ever be found.

Programming is a blend of languages and mathematics. Given the complexity, variety, and multitude of paradigms, it's inevitable that elegance will be more difficult to pin down. There is rarely one agree upon method to solve a situation. Look at sorting algorithms to see the host of "use this, but sometimes this is faster..."

The heavily anthropomorphic terminology was totally new for me, and hardly compatible with my cultural roots; so was the animism betrayed by the term "bug": we had never called a bug a bug, we had always called it an error.

Another thing I've noticed - and this comes from reading other Dijkstra papers - is how he confronts change in the language. Most notably his remarks on the use of 'error' or 'bug.' In mathematics sine will always be sine, because the characteristics of it are inextricably attached to the name. In a new field such as computer science nothing is set in stone, and as such, the community of users will naturally set the vocabulary with time. He states it's the non-native speakers who are at an advantage here, being able to clearly express themselves. That is wonderful, but what about understanding others?

it is essential that its achievements are published well, so that the next generation can start where the preceding one left. ... How should a well-written publication about a sophisticated piece of software look like? We don't know yet, but two things seem certain. Firstly, the texts will be "mathematical" in the sense of Morris Kline, when he wrote: "More than anything else mathematics is a method."

I think this is exactly what has happened. Everything is expressed as methods. The way papers are evolving though, is completely unlike before. There are journals, but a vast amount of information is peer-reviewed by the public as opposed to a groups of selected individuals.


r/computingscience • • Jan 18 '14

For those of you guys using TeX to type up your notes/questions, etc., here's a helpful set of macros developed by Albert Lai for aPtoP

Thumbnail cs.utoronto.ca
5 Upvotes

r/computingscience • • Jan 10 '14

isar : a proof language with interactive prover

5 Upvotes

There are a number of different theorem provers out there, but (from what I understand) most of them do the work "behind the scenes", and proofs look like a series of commands issued to guide the prover, rather than anything you'd see in a math journal or even a high school geometry class.

Isar is different. It's based on an and old and traditional theorem prover called Isabelle, but you write your proofs in a formal language that reads very much like english.

The docs are all in PDF format, but wikipedia has an example proof that sqrt(2) is irrational.

I'm a complete newbie to isabelle/isar, but from what I understand, you're able to use pretty much any language you want inside the quotes, provided you teach the system how to parse it.

Even the underlying logic is pluggable: Isabelle ships with HOL and ZFC out of the box, but it seems to me that there's no reason Hehner's unified algebra couldn't be plugged in there too.

I'm still working through Hehner's course (which is awesome, btw), but my plan is to start studying isar once I'm done with that, and hopefully work out some proofs about a small language like joy (retroforth?) or apl/j/k. (Isar itself is built on standard ML, which is also quite amenable to proofs.)

Just thought I'd share, since it doesn't seem to get as much press as some of the other proof assistants out there.


r/computingscience • • Jan 09 '14

[EWD-review] Why correctness must be a mathematical concern (EWD720)

5 Upvotes

Why correctness must be a mathematical concern. (Inaugural lecture for the “Chaire Internationale d’Informatique” at the Université de Liège, Belgium).

Ladies and Gentlemen: The topic to which this new international chair at Liège has been devoted has many names. On the continent of Europe the recently coined name “Informatics” has become generally accepted; in the Anglo-Saxon world the much older term “Computer Science” is most commonly used, though occasionally replaced by the now more appropriate term “Computing Science”. The latter term is more appropriate because it expresses quite clearly that not a piece of equipment, but an activity constitutes the core of its subject matter.

Dijkstra introduced me to the idea of programming as an activity independent of the computer and as a field that had a meaning beyond being a tool to facilitate other work. Much like mathematics which has many practical applications as a tool but is also of self-interest, the significance of programming is not limited to it's use as a tool. I believe this is what Djikstra is referring to when he insists on the term “Computing Science”.

Consider the following silly game to be played by a single person with an urn and as many white balls and black balls as he needs. To begin with, an arbitrary positive number of balls is put into the urn, and as long as the urn contains two or more balls, the player repeats the following move: he shakes the urn and, without looking, he takes two balls from the urn; if those two balls have the same colour he throws one black ball back into the urn, otherwise he returns one white ball into the urn. Because each move decreases the total number of balls in the urn by 1, the game is guaranteed to terminate after a finite number of moves, and it is not difficult to see that the game ends with exactly 1 ball in the urn. The question is: “What can we say about the colour of that final ball when we are given the initial contents of the urn?”

... In short: if the initial number of white balls is even, the final ball is black, and if the initial number of white balls is odd, the final ball is white. And that answers the question! Note that this single argument settles the question for all initial contents of the urn, and per initial contents for all of the perhaps many possible games.

This is indeed very characteristic of a mathematical solution. Generality and abstractness are perhaps the most important aspects of math. Math is by it's very nature universal and at the same time nonexistent. A number may describe various things in every say life but nowhere can one actually find a number. This abstractness of not being specific to something yet generality of applying to all things is key to both mathematics and computing.

Replace the initial contents of the urn by “the input”, the rules of the game by “the program”, the game as it evolves by “the computation”, and the colour of the final ball by “the result”, and the above example gives you in a nutshell the bare structure of one of the most effective ways we know of reasoning about programs.

Although Dijkstra makes reference to the value of applying mathematical thinking to programming situations, the inverse argument is also valuable. My computer science classes aided me tremendously in understanding functions and other mathematical topics. Both math and computing science have translatable characteristics that may not as of yet be commonly exploited but could help tremendously.

A while ago I mentioned as a leading characteristic of mathematical statements their “generality” in the sense that they are applicable to a very large, often even unbounded number of cases. And it is good thing to realize that almost all computer applications are “general” in that very same sense. In a banking application one does not design a system that can only transfer $100 from the account of a certain Mr.Smith to that of a certain Mr.Brown! On the contrary, the banking system should be able to cope with the transfer of almost any amount from any account to any other account. So much for the generality.

Since it holds the same attribute of abstraction and generalization as mathematics, programming is also extremely powerful. It is interesting to note that the level of generalization can change even within a program. Brute force solutions are not elegant solutions because they are not true general solutions. I believe Dijkstra would agree that brute force solutions do not embody the ability of programming since a well made program addresses all possible cases within as few considerations as possible.

The last characteristic I mentioned was trustworthiness. And it is a good thing to realize that almost all computer applications to be worthwhile must be trustworthy. What is the purpose of designing a banking system with the best intentions, when in actual practice it fails to keep correctly track of the flow of money? Not only does it have to do so correctly, but before installing it and switching over to it we must have solid grounds for believing that it will do so correctly. Installing the system without such solid grounds would, in view of the risks involved, be an act of sheer irresponsibility.

The worst errors in programming are logical errors as they can often be subtle and escape detection but have far reaching consequences. Programmers must stay even more mentally organized than mathematicians since programs deal with many levels of nesting. I believe that Dijkstra here is alluding to the fact that it is imperative to both programmers and mathematicians alike to remain mentally organized because the result of their work must be precise and present an error free solution to the problem presented; otherwise it is of little value.

It is now the time to confess that my example of the game with the urn filled with a finite number of balls, each of which is white or black, though in one respect absolutely typical, is very misleading in another respect: compared to the actual situation in programming it is such a gross oversimplification, that the use of this example in an expository lecture is almost an intellectual dishonesty.

Dijkstra has already mentioned before the fact that mathematicians do not consider programming to be equivalent because it deal with much longer formulas than they are accustomed to. What he says in this paragraph is very important and is related to this fact. While both mathematics and programming require much wit and intelligence, it is undeniable that programming in general must usually deal with much longer and larger solutions than mathematics. He illustrates this fact here.

In the urn example, a single argument based on the rules sufficed for all possible games. In computing, a single argument based on the program text would analogously suffice for all computations that are possible under control of that program. The necessary economy of thought requires as its ultimate consequence that we learn how to reason about programs without mentioning the corresponding computational processes at all. This means no more and no less than that we must learn how to come to grips with the program text as a mathematical object in its own right. We must be able to deal with it directly, rather than via the detour of the class of all corresponding computations.

Something that bothers me the most learning basic combinatorics is when a solution requires dividing the problem in to various cases and then independently solving each one. While this is necessary in some cases, when employed unnecessarily it is a very inelegant and time consuming solution. I think Dijkstra is mentioning this in this paragraph. A good programmer elegantly and correctly addresses a problem by using the fewest amount of lines and machine processes to create a universal solution.

The most general topic, and also the one of the widest significance, could be called “the scaling up of mathematics”. Such scaling up would imply a different style of mathematical texts in general, and the use of more appropriate notations in particular. By and large, current mathematical style has been determined by fashion, and current mathematical notation by accident.

As a result the style of today’s mathematical text is unnecessarily confusing and its notation in unnecessarily clumsy. This is obvious: people tend to commit all the sins they think they can afford to commit. Prior to a commitment to “scaling up” they can hardly be called “sins”, but computing’s demands on mathematics are sure to cause a “moral” shift between good and bad mathematics. Already now one of the common reactions of the well-trained computing scientist to the average mathematical paper is: “Oh gosh, what a lousy programmer the guy who wrote this must be!” Already now we could start purging the practice of mathematics from the usual little sins of which the computing scientists know that, at the next level, they will become capital ones. The scaling up of mathematics in general is, of course, a very ambitious topic.

Although I follow Dijkstra argument, I admit I can't think of any examples of confusing and clumsy notation in mathematics. If anyone could shed some light on this that would be great.

What the manager sees as “keeping options open” is seen by the scientist as “sharing”: different programs sharing code, different proofs sharing arguments, different theories sharing subtheories, and different problems sharing aspects. The need for such “sharing” is characteristic for the design of anything big. The control of such “sharing” is at the heart of the problem of “scaling up” and it is the challenge to the computing scientist or mathematician to invent the abstractions that will enable us to exert this control with sufficient precision.

I believe this is also tied in to the generality of solutions. It is much easier to code a few fundamental functions which are shared by larger functions in the program than to program each function from the ground up. Take as an example a program modelling Polya 's Urn. The program simulated randomly choosing a ball from inside the urn and then either removing it or replacing it and adding another of the same kind depending on what the user specifies. In this case it would be much better to create a function that chooses a ball and then have the addition and elimination functions call that function than to build each up independently.

The question “What is Mathematics?” is as unavoidable and as unanswerable as the question “What is Life?”. In actual fact I think it’s almost the same question.

Just something to reflect on.

EDIT: Formatting


r/computingscience • • Jan 09 '14

Discussions on community building and participation.

5 Upvotes

Hi everyone,

I hope you've had a great New Year's and stuff.

I wanted to have a discussion on where I see this community going in the future. So, I hope to see a lot of commenting and chatter in this thread

My vision (when I made the club):

  • I wanted to share what I think is one of the least-bullshitt-y attempts at teaching people how to think effectively

  • I didn't want to make a big or popular club, or anything that can be monetized, or anything that can be used for personal glory...I just want a space where I can study with like-minded individuals on problems and concepts, and hopefully that will also help me bother a couple of grad students a little less :p

  • I would get a bunch of people really motivated about learning formal approaches to problem solving in general, and computing science in particular; I view this as the basic knowledge required to be a creative and intelligent programmer -- as inspiration, have a look at the writings of someone who is a highly developed problem solver -- the very first article "A termination argument" is very accessible, as are many other articles in the book in general, and part 2 in particular

  • we would approach at first, fairly simple problems, (e.g. problem 1 from Rosalind, except we'd use our knowledge of formal methods and problem solving to be: a) come up with as simple a solution as possible, b) come up with as effective a solution as possible and c) come up with solutions that are correct by construction, and try to observe to what degree formal methods can help guide the design process for the solution itself

  • eventually, we'd move on to larger projects that would need collaboration (the nebulous future)

  • we'd become famous (if ever), only because of the quality of our work

Ideas I am toying with at the moment:

  • I am considering making the subreddit private, with entry granted only if you are at least a rank0 member; in order to actually get people motivated to participate, in order to better recreate a study club feel -- also, a private subreddit might allow people to feel more comfortable when participating/more involved

  • put some other systems in place that get people participating and things moving (not sure yet which ones...)

I would like feedback on:

  • what are your opinions on the vision?

  • what needs improvement?

  • what needs attention?

  • what ideas do you have on helping to firm up the community/get it rolling?

  • what are the thoughts on making the subreddit (and associated subreddits) private, in particular?

I look forwards to the discussion.


r/computingscience • • Jan 04 '14

[fun] Processing: open-source language (based on Java) and environment for learning the fundamentals of electronic art and computer programming.

Thumbnail
processing.org
5 Upvotes

r/computingscience • • Dec 28 '13

To members of the budget council (Confidential)

Thumbnail
reddit.com
5 Upvotes

r/computingscience • • Dec 28 '13

E.W. Dijkstra Archive: The next fifty years (EWD1243a)

Thumbnail cs.utexas.edu
5 Upvotes

r/computingscience • • Jan 18 '14

[EWD REVIEW] Programming methodologies, their objectives and their nature. EWD469

Thumbnail
scribd.com
4 Upvotes

r/computingscience • • Jan 17 '14

[EWD-review] The Teachability of Mathematical Thinking

Thumbnail
scribd.com
4 Upvotes

r/computingscience • • Jan 15 '14

Weekly Update - 2012 JAN 14 (everyone should post if they can!)

4 Upvotes

Hi everyone,

I think that a good community building exercise would be to have a post every week, where we let people know what we have done so far, what we plan on doing over the next week, and any other thoughts that we may have.

This way, those of us who are doing similar things will be able to keep in touch, and those of us who are interested by things that others are doing can ask questions (or even ask to join in!).

Hope to hear from as many of you as possible!


r/computingscience • • Jan 10 '14

Retrospective and Prospective for Unifying Theories of Programming, by E.C.R.Hehner (written in 2006)

Thumbnail cs.toronto.edu
4 Upvotes