Lambda the Ultimate

I see the cryptographic community making proofs on code they write. I see static analysis used to validate certain properties of "simplified" C in "real" embeded systems but how much business is really done that uses formal methods to support their development.

Now the reason I mention this, and this is not new, that there has always been a chasm between the "academic" understanding of using mathematically oriented ideas to do things with software and the real life of hiring a developer to get a project done.
I was wondering if this community felt that things were improving.

My personal experience is not good but I will admit that looking at others I am feeling a bit more up-beat these days. Any one want to share their thoughts?

This paper seeks to explode the myth that Turing Machines (TM) are the universal model for all computation.

Church-Turing Thesis: Whenever there is an effective method (algorithm) for obtaining the values of a mathematical function, the function can be computed by a TM.

[...] The Church-Turing thesis has since been reinterpreted to imply that Turing Machines model all computations, rather than just functions. This claim, which we call the Strong Church-Turing Thesis, is part of the mainstream theory of computation. In particular, it can be found in today's popular undergraduate theory textbooks:

Strong Church-Turing Thesis: A TM can do (compute) anything that a computer can do.

It is a myth that the original Church-Turing thesis is equivalent to this interpretation of it; Turing himself would have denied it. [...] In fact, the Strong Church-Turing Thesis is incorrect - the function-based behaviour of algorithms does not capture all forms of computation. For example, as explained in [Weg97], interactive protocols are not algorithmic.

[...] The reasons for the widespread acceptance of what we call the "Turing Thesis Myth" can be traced to the establishment of computer science as a separate discipline in the 1960's. To understand these reasons better, we can identify three distinct claims that make up the myth, and examine them individually:

• Claim 1. All computable problems are function-based.
  • Reason: Adoption of mathematical principles for the fundamental notions of computation, identifying computability with the computation of functions, as well as with TMs.
• Claim 2. All computable problems can be described by an algorithm.
  • Reason: Adoption of algorithms as the central and complete concept of computer science.
• Claim 3. Algorithms are what computers do.
  • Reason: Broadening the concept of an algorithm to make it more practical.

Each claim is then explained in detail, and refuted, along with a few other corroborating claims. The paper concludes with an extension to TMs to model interactive computation.

Hi,

in front; sorry for my broken english. I'm german and my english isn't very well.

Sinces days, i try to embed eclipse/prolog in a VC++6 application, but there are many problems with it.

I wrote some classes for a console applikation and everything works beautiful. Now i want to use this classes in a MFC - Window application. Everytime I start the application, the system stopped for a long time while calling the eclipse-command and the result isn't correct too.

I think it depends on the missing Console witch eclipse need to interact. Have someone experiences with it?

Its real hard to find someone to talk about it.

thanks
Nukleo

Even in a lazy language like Haskell, lifted boolean operators like 'and' are not commutative. What I mean is that they're commutative only as long as bottom is not involved. In that case, for example, 'and' and 'flip and' are not interchangeable. This causes problems in certain applications like trying to simulate certain cyclic logic circuits. To a great extent you can avoid these problems by carefully thinking about which input to 'and' you want to use, but I'm interested in designing a system where this is not necessary.

I've just finished coding up a system that has a commutative and. It consist of two parts: a new 'and' called 'land' that uses Maybe Bool as its data type and a discipline for programming with 'land' that requires you to iterate until you find a fixed point before returning a result.

I'm looking for some references to papers, books, web sites, etc. that might help me understand more about this topic and not reinvent the wheel any further than I already have. I'm also interested in the generalized version of this topic, i.e. beyond boolean operators: "when conventional laziness just isn't lazy enough." I've done some Googling but haven't seem to hit upon the "magic words."

i have got a gmail
thanx guys

For a while, I've been awaiting a scholarly book on the topic of virtual machines. Bill Blunden's book ain't it; and the other books (until recently) which were relevant were all practical works on particular VMs, usually that of Java or the MS CLR.

Now, it appears that two textbooks on the topic are in print: One is Iain Craig's Virtual Machines (ISBN:1852339691) published by Springer; the other is Virtual Machines: Versatile Platforms for Systems and Processes by Smith and Nair, (ISBN:1558609105), published by Morgan Kaufmann.

Judging strictly from the summaries at Powell's website; the former appears to be a slightly more academic treatment of the topic; the latter looks a bit more practical-oriented. (I'm interested in both). The latter also seems highly concerned with topics like CPU emulation and OS-level virtual machines (like VMware), as opposed to VMs as a programming model/programming language runtime (like JVM or CLR). A summary is here.
I couldn't find any in-depth reviews of the Craig book online, especially from reputable reviewers.

Has anyone read either book (someone mentioned the first one in another thread), and have any recommendations, pro or con? The second book is on the shelf at Powells, so I might go check it out. The first book is on backorder.

Thanks!

From Yearning for a practical scheme - "I don't want to load a SRFI

I do wonder about the scalability of CL or Scheme along the number-of-coders axis. When you have 20+ programmers working on code that was originally written by a separate group of 20+ programmers... The limitations of a language like Java might actually be a benefit in these

This is an issue close to my heart, and one that I think the LtU under-discusses. First of all, a few confessions: I am a Haskell afficionado, and hate Java with a passion for the mindset that it promotes, where coders become nothing more than LoC mincers. It saddens and angers me that people are wasting time learning it, because there is nothing in Java (or C#) that is new; and old in them are botched and bungled. That said, however, I have started to appreciate them in a different capacity.

I've recently started a position with as a lead and architect, and so also manager. After floundering for a bit, I started to think like a manager (much to my regret). The business reality is that most "programmers" (and I use the term loosely) are not LtU material. They probably didn't see the symbol lambda during their university educations. Furthermore, asking them to understand the intricacies of CPS transforms and endo-hylo-cata-ana-expi-ali-docious morphims. They wouldn't be interested either. Most programmers are just Java monkeys; it arises from the fact that there are more people than can competently (by our standards) program who are willing to take the salaries that the industry offers. Doubtlessly, if they did not work in the industry, the industry as a whole would produce better work (though not more work; more on this in a minute). The wages would also be higher... which would then attract them right back. The fact is that we count competence in terms of elegance and a feeling that a piece of code will last -- a Mona Lisa of the pyramids. The customers of our industry, however, does not hold us to such high standards. They are happy to spend less time looking for their data. They are really happy when you can save them even the smallest bit of time. They will also be satisfied with a poorly written piece of shit that passes the basic mustard. This is the reality, and no amount of Mary Poppins impressions will change that.

These problems plague all fields, engineering especially. There is one main aspect in which we stand out, which is that we deal with more complexity than any other field. Other industries struggle with structure more than 20 or 30 layers deep, while we brush them off and imagine towers so tall that we can't imagine any further. We then build them, and see how we can build even taller. I estimate (also known as pulling numbers outta my ass) that we deal with 100 times more layers of structure than any other field. In a way, it can be said that software engineering is all about complexity management.

Which brings me back to Java. It, as a language, sucks. Its one redeeming feature is that it is a lowest common denominator. I could get my English majoring friend to learn it. At first glance, the language itself is poor as hell to manage complexity. Surely the fact that you need tens of files just to equal a page of Haskell already represents a huge LoC count? Not to mention readability? Yes, in my opinion. But that's also not where Java shines. Indeed, Java is less about programming and libraries and so on, and more about the processes which are built around them. Everything from the consistency of presentation of documentation to universality of training schemes that exist. These are extra-language features that have made it popular. It is also, AFAICK, the first language that was commercially pushed successfully. These things we cannot ignore.

The first lesson that I learnt doing project management, is that a project is less about the technologies, even less about the product, and almost all about the team. The people that make up the project are the project. If you are lucky that you've got a crack team of PL specialists and who are also experts in the problem domain, then you will succeed. But you're never going to get that. At best, you will get 10 Java monkey level people, and 1 who can grok the difference between structure subtyping and nominal subtyping (not in those words, however). This is where the Java processes become invaluable -- they've laid out all the correct procedures that you, as the lead, should do to get everyone to work together. You draw some UML diagrams, etc and just generally follow the road. At the end of the day, if it fails, you can simply say that as an industry, you weren't ready to take on the challenge, and be absolved of personal responsibility. Furthermore, it also helps you with planning -- how many packages, how many components, how many classes == how many man-hours == easy calculation of projected costs and timescale. These are the things that the customers care about, and it is a rare customer that cares even about "maintainance" costs, where you'd have some leeway to build in some reason to sneaky something good in. Oh, and the worst thing is that most won't even care about that -- they'll ask about risk, which forces you to justify any and all choices, especially ones perceived by the local "expert" as outliers.

On these fronts, Java stands unrivalled (except for C#, which for the moment is almost the exact same). It makes economic sense. It also makes no sense in any other way. If I get a Lisp guru to hack up some code, the resulting poetry will be unutterably beautiful, and will take another equal guru forever to read it, all the while exclaming the great use of macro transformers. It becomes a single person pursuit. There is nothing wrong in general with single person endevours, but there are times when you need to get something done quicker than one person can, and then you need more people to help.

Thus we are back at the beginning. We have unimaginable complexity, and we have people who can't comprehend it. We do need formal processes to help us. So far, the only successful industrial scale ones have been extra-language. I wonder if it would be possible to bring them into the language? In other words, to have the language incorporate a framework to help with the workflow? I've personally tried to control the complexity by using industry standard protocols to set out the edges of components and hoping that each component can be done by one person. I have a feeling that there is always going to be a gap between those who can see the system in the whole, and those who will be working the trenches; I also find it unsatisfactory. I also don't have any better ideas.

The Anatomy of a Loop by Olin Shivers

…the lexical-scope rule of the classic λ-calculus, which we’ll call “LC scope,” implies an important property: it ensures that binders dominate references. The key design idea that serves as the foundation for our extensible loop form is to invert cause and effect, taking the desired property as our definition of scope. This gives us a new scoping rule, which we call “BDR scope.”

From this concept, Shivers builds a sub-language for describing iterations which includes what is effectively a directed graph of scopes, rather than a simple tree. Parallel code paths (or perhaps a better description would be unordered code paths) can independently contribute to the binding scope of following code, without being visible to each other. (See the example of quicksort on page 11.)

Is this too wierd for real programmers? Or is it a stunningly elegant way of capturing something important about parallel code flows? I vote for the second but I wonder what other LtUers think

(Via the JML list.) The docs are skimpy, but they claim to extend "environments with type systems, which provide an automated means to enforce many basic policies, and use the resulting framework to cover a wide range of security policies for global computers."

Through their global, uniform provision of services, and their distributed nature, global computers have the potential to profoundly enhance our daily life. However, they will not realize their full potential, unless the necessary levels of trust and security can be guaranteed.

We aim to develop the technology for establishing trust and security for the next generation of global computers, using the Proof Carrying Code (PCC) paradigm.

Found this linked in the comments section of an interview with Charles Simonyi

http://www.cse.unsw.edu.au/~cs3141/ip.asf