Lambda the Ultimate

Whether or not such would be always be called PLT is somewhat arbitrary.

Good point. It is difficult to see where the 'language' stops.

I tend to lump Operating System and Programming Language and Protocol together as being the same 'sort' of thing, given their often tight relationships. Language environments such as SmallTalk and Lisp add credibility to such an aggregation, and LtU and C2 have each had a few discussions on the subject [1][2][3]. To clarify: by 'Operating System' I refer broadly to all runtime and architectural expectations, such as presence of File Systems or Databases, UI integration, organization of Shared Libraries, support for a Dynamic Link Loader, the Process model and IPC, etc.

I think it useful to take a sort of Systems PLT (ref Systems Biologist) view. When understanding a language, we must treat the language and its environment as a components of a gestalt, and model the interaction. And come design-time, we must design the language and environment, and their interaction.

Many language designers see "design the environment" as an almost ludicrous task. After all, a language must work in the environment that exists today to be 'practical', does it not? Why, designing the environment is almost as ludicrous as blasting holes through mountains to support railways, or laying roads to support vehicles. Why, that's nearly blasphemy! heresy! So many language designers adapt their languages to the expectations of the existing Operating Systems, FFIs, existing Web Services and Browsers and HTML and HTTP protocols, existing Databases and popular Query Languages (read 'SQL')... instead of vice versa.

I think this unfortunate. Many such languages are window dressing for the environment, utterly interchangeable, bikeshed coloring. They perhaps address a few syntactic grievances, or enforce a few useful properties, and I won't say this is useless: appropriate syntax and appropriate abstractions may result in a better economy of expression. But, to whatever degree the environment imposes itself upon the language, you must ultimately express the same abstractions as the environment forces upon you. And, today, those abstractions are far from optimal.

Economy of expression simply isn't enough. I probably spend a minority of my time actually writing code, and much more performing testing and debugging, maintenance and upgrade, documenting, requirements analysis, configuration management, integration with live systems, and so on. To get the most bang, these processes must be eliminated wherever possible and optimized everywhere else. (Separate 'installation' and 'build' steps, and 'packages' and 'binary ABIs' are not essential complexity.)

For efficient Software Engineering in-the-large - to "improve the overall economies of the endeavor" - we must change the environment - lay roads and demolish mountains as necessary.

This can be done incrementally. There are well-known patterns to allow a languages to operate in a hostile environment - one that violates the language's expectations. For the language local runtime, you can introduce a VM atop the OS. When dealing with 'remote' elements of the environment, such as browsers and servers and dynamic HTML and HTTP, you might introduce plug-ins, adaptor layers, or even provide whole new browsers and servers. To deal with firewalls, or alternatives to socket-based communications, or different networking expectations, you can introduce overlay networks.

But I suppose there is a lot of inertia, and changing the environment is a daunting task.

I tend to lump Operating System and Programming Language and Protocol together as being the same 'sort' of thing, given their often tight relationships.

I agree! OSes, PLs and Protocols are all services i.e. systems that (a) perform useful functionality, and are (b) invokable according to a particular interface.

It's too bad OS designers couldn't realize this sooner and design the OS with that in mind! Then, software would be given proper treatment, as a set of invokable services, rather than as sets of instructions to run in one or multiple files! The past several decades have been spent fixing that problem, trying to shoehorn our mismatched old definition of software into the proper model of software as services! Examples include 'NIX's pipes and command line utilities, and Microsoft's OLE and COM models. Even IBM has done work on that. I lament.

Could you be more describe more precisely what you would change?

The Paradigm:

First, the definition of software needs to be roughly "one or more invokable services." We need to change our perception of software to match this definition.

The Architecture:

Second, one needs to change the OS to NOT run executable files, but rather, each software installation automatically registers into the system, the invokable services of the software, under a namespace. The code for the services would be stored in one or more modules/libraries.

Some of the services provided by software would be automatically recognized by the OS for carrying out specific functions, e.g. shell presentation, opening a GUI front-end for users to use, etc.

Others could, for example, be recognized by other, custom-made service systems, or something.

But the main idea is that the OSs architecture is designed to seamlessly support a service model of software from the ground up, and to NOT support the idea of software as one or more executable files! Not only to support this kind of model, but to actively orient itself towards this model. Everything becomes a service. The OS could have its own scripting language that can tap into all services, and in turn, define more services.

So, it is a much more programmable OS, I suppose.

I realize that OSes have been evolving toward this type of functionality for years, perhaps serendipitously so, but we need this shift in perspective if we are to grok the better sense of this approach.

...I like unixy things that are obviously written by programmers for programmers with the expectation that a large part of your productivity is geared to creating programs by using programs.

For example the most potent data file format I use is... Ruby! Way more flexible and expressive than CSV or XML.

each software installation automatically registers into the system, the invokable services of the software, under a namespace
I can't see what "registering" in a name space would give you over and above the existing path lookup insert into hash scheme modern shells use.

I truly _love_ the unixy "Everything is just a file, and a file is just a stream of bytes" paradigm.

It's remarkably simple yet powerful. You'd have to have a wondrously compelling argument for me to ever willingly move away from it!

I haven't done away with files, I've done away with executable files, and replaced them with invokable services.

And, what's so bad about everything being integrated anyways?

Take gcc for example.

Install gcc and what do you get? The gcc master executable is the one you want the user to use 99.999% of the time. Inside the directory tree are _many_ sub-executables that mostly (but not always) gcc invokes for you.

Directories create a heirarchichal namespace for you that _always_ aligns with the file level "not there / is there / moved over there". Registries accumulate cruft.

And integrated with what? I have probably over 6 versions of gcc (different version numbers different processor targets) on my box.

Service-oriented architecture is about processes.

However, much of what IBM creates for you with its "Web Services" is actually (remote) procedures (calls) and processors (Red Hat's work on "restful transaction managers" [the most absurd abuse of marketing buzzwords] is a good example of such monolithic thinking, where the manager is a processor and the so-called REST API is really a way to PEEK AND POKE at the processor's context).

In compiler architecture terms, you are invoking a process step or the process step can be treated as its own process. See the CoSy compiler architecture as a reference example; this work was done in the '90s as a radically different way to structure compilers and break free of monolithic gcc-like architectures. An argument could be made that CoSy does the UNIX-model-as-John-Carter-describes-UNIX better than UNIX does.

Directories create a heirarchichal namespace for you that _always_ aligns with the file level "not there / is there / moved over there". Registries accumulate cruft.

This could just as easily be restated as directories create a hierarchical namespace that allows out-of-band communication between the user and the system.

[Edit: For references to CoSy, see Alt's Ph.D. thesis On Parallel Compilation and his associated papers on CoSy.]

I think it is hard to compare these two things. For example, Maxwell and Navier-Stokes are "god-given" (or Maxwell-given or whatever). If you work in this field, you cannot do without them, because they describe certain facts in the best way known to mankind for describing basic physics, which is mathematics.

Nobody needs Petri nets, message sequence charts, live sequence charts or statecharts to build software. This is just complicated notation for pretty simple things. Whereas Maxwell is pretty simple notation for pretty complicated things.

Your point seems to not have any detail sentences, but rather meant to be taken as statement of fact.

I'll do my best to clarify why I cited that quote, though, and why I like it.

If you work in this field, you cannot do without them, because they describe certain facts in the best way known to mankind for describing basic physics, which is mathematics.

You cannot do without them because (a) they are formal and rigorous (b) useful models (c) simple.

Nobody needs Petri nets, message sequence charts, live sequence charts or statecharts to build software.

You are right - building software is something a teenager can do. Anybody can bang their head against the keyboard and call it Perl. Engineering quality software is something a formally trained professional should only be entrusted to do; see CAR Hoare's recent recommendation to the British Royal Academy that more software engineers require a minimum level of proficiency in certain areas to work on certain projects.

This is just complicated notation for pretty simple things.

It is true that the degree of freedom visual notations allow for arranging entity types is complicated, and that fewer degrees of freedom can make interpretation of syntax more consistent. However, strategies like the Barker technique for positional notation - following the "Crow's Foot Rule" - actually simplifies the notation and imposes consistency on the representation. The underlying degrees of freedom are still there, but the representation is the way it is because it maximizes the human brain's throughput several orders of magnitudes moreso than text. Syntax is part of communication. Joseph Goguen (creator of the OBJ family of languages that inspired Maude) once wrote a great paper where he coined the term semiotic morphism to describe preserving meaning between two representations of the same thing. He then said that if the translation is lossy, you should strive to preserve structure and then content. On the subject of visual communication, I would also recommend Edward Tufte and Stephen Few.

I would also argue that Statecharts are not a notation for "simple things", and that use of a statechart implies some sort of composition is taking place. Topologically, this might suggest refining the model using pointwise reasoning. In an object-oriented view, such composition might suggest refining the problem domain into a better terminology (more objects, each with different roles), because composition generally means some very large responsibility is taking place that centralizes behavior into a single common structure.

For Petri nets, it is true that to model software you generally do not need the use of anything more general than finite state automata, and sticking with FSA as a default is a great design choice, since it forces you to think more modularly. It is entirely possible to also use another model for bigraphs. Petri nets are not just a notation, but also have semantics (e.g. Run-To-Completion requirements).

Message sequence charts describe 'connect the dot' information. What that gives you is a degree of freedom between (a) dynamic collaboration between senders and receivers (b) between dynamic collaboration and messages (c) between messages and individual object's methods. Statecharts can then in theory be used to show what the system actually looks like when those dots are connected.

Anyway, I don't actually build systems this way because the biggest problem we face is customization ("software factory" and "software product line" problems), not language semantics problems.

Whereas Maxwell is pretty simple notation for pretty complicated things.

Maxwell Equations are about semantics, not notation!!!! Many mathematicians have given a different notation for them.

I just think that computer science (the software branch) has not arrived at a comparable level (compared to physics) of sophistication yet. Maybe it never will. Because in physics we are bound by the laws of nature. With software, we are bound to a much lesser degree by the laws of nature, and to a much higher degree by our imagination. Therefore I think that too much formal education is dangerous. As an example, look at all that research that has been done into types. Yes, Hindley-Milner is useful. The rest of type theory that this has started, not so much :-)

You may say that the above is too philosophical and that the industry needs formally trained software engineers. I am not going to argue about that. I don't care much about "the industry". I know that I cannot trust the software in a plane, and I do not see a good way to change this now. I will still use planes now and work on topics that will solve this problem in a couple of decades from now.

With software, we are bound to a much lesser degree by the laws of nature, and to a much higher degree by our imagination.

Not really. Information is bound by laws of nature as well, and what is a program but expression of the structure and evolution of information?

Yes, Hindley-Milner is useful. The rest of type theory that this has started, not so much

I don't see how this is supportable. There has been significant evolution beyond HM. You need only look at Haskell for proof.

So what is the improvement of Haskell. That for example type classes allow us sometimes to do things we have always been able to do without static type checking?

Yes, that you can push an ordinary programming extraordinarily close to theorem proving, whilst retaining expressiveness and compositionality in a relatively simple package. Haskell has made significant progress here, with type classes, GADTs, and monads being primary contributions to this end. Usable static checking of properties of any kind is a significant advance over doing it without static checking.

When will Haskell-like static checking be useful in practice for a large class of software? Currently either the guarantees are weak or you need to prove theorems manually. In both cases the bugs eliminated/effort ratio is small compared to unit testing (especially random testing like quickcheck).

We need a strong optimizing compiler that can prove theorems by optimizing quickcheck properties like "rev (rev xs) == xs" to "true". This is feasible with current (but not mainstream) compiler technology.

We need a strong optimizing compiler that can prove theorems by optimizing quickcheck properties like "rev (rev xs) == xs" to "true". This is feasible with current (but not mainstream) compiler technology.

You mean something like this? Perhaps greater static checking is possible, but Haskell and some minor extensions already get us pretty far.

Exactly. Very interesting, but it's a pity they don't discuss limitations.

They do towards the beginning IIRC. Basically, any pure Haskell terms can appear in contracts, with the caveat that the contract checker may not be able to prove they are converging and so you may get a "can't determine whether contract satisfied". The quintessential example they used was "prime x > sqrt x". See section 2.2.

This approach strikes me as being very close to an abstract interpretation of the program, and it seems a shame that type checking and contract checking can't be unified into a single mechanism. I also don't think there's a mechanism where you can introduce lemmas to help you prove undecidable properties, so that's an obvious extension for future work (perhaps strengthening the "ensures" properties of any functions used have a similar effect?).

As a final thought, this work very closely resembles Microsoft's Code Contracts library for .NET 4, so I wonder if they snatched up the developer who worked on this.

More limitations are needed. To me it is not clear where the line between what they can do and what they can't do is. Can they prove "rev (rev xs) == xs". Can they prove "tailrecursive_rev xs == ordinary_rev xs"? Can they verify the correctness of an exact cover solver? Etc. until the examples are too difficult for their system. prime x > square x is a limitation in their auxilary theorem prover, not in their core system.

Also related is partial evaluation, supercompilation and generalized partial computation. Microsoft Code Contracts seem stronger on the theorem proving side but weaker on expressing contracts in the language itself.

Unifying types and contracts would be very nice. If types are predicates (e.g. is_int) in your language then they can be handled in the same way as contracts. Polymorphic types are higher order predicates (e.g. list(is_int)). But how do we deal with function types and mutable cell types? Can we just adopt the existing contract work or does this lead to problems?

The sage project comes to mind http://sage.soe.ucsc.edu/

This approach strikes me as being very close to an abstract interpretation of the program, and it seems a shame that type checking and contract checking can't be unified into a single mechanism.

Perhaps I'm missing the obvious, but AIUI this has been done. In the type-theoretical literature, contracts are called "refinement types".

Refinement types can also be handled by using the propositions-as-types correspondence, as long as proof irrelevance is available.

See:

1. Freeman, T.; Pfenning, F. (1991). "Refinement types for ML". Proceedings of the ACM Conference on Programming Language Design and Implementation. pp. 268–277.
2. Hayashi, S. (1993). "Logic of refinement types". Proceedings of the Workshop on Types for Proofs and Programs. pp. 157–172.
3. Denney, E. (1998). "Refinement types for specification". Proceedings of the IFIP International Conference on Programming Concepts and Methods. 125. Chapman & Hall. pp. 148–166.

Yes, but for some reason I had thought refinements weren't quite ready for prime time. Jules' Sage link has papers implying otherwise.

this work very closely resembles Microsoft's Code Contracts library for .NET 4, so I wonder if they snatched up the developer who worked on this.

See the bottom of Microsft Research's Code Contracts project page - Project Members.

In their papers, the Code Contracts team does of course cite Dana Xu work under SPJ on static contract checking. However, the Code Contracts team also have papers where they argue for exactly why they did certain things a certain way, such as choosing to embed Code Contracts into the method body as opposed to elsewhere.

e.g.

using System;

class Test
{
   public static void Main()
   {
      Do("test");
   }

   private static void Do(string s)
   requires s != null;
   {
      Console.WriteLine(s.Length);
   }
}

or alternatively, using "bang" syntax specific to non-nullability:

using System;

class Test
{
   public static void Main()
   {
      Do("test");
   }

   private static void Do(string! s)
   {
      Console.WriteLine(s.Length);
   }
}

You might be saying, "Z-Bo, you are arguing about syntax". Actually, that is not what the argument is about! While it is true that the above code requires adding static production rules to the compiler's infrastructure (C# -> Spec#), and therefore complicates the implementation of compilers, there is another way to look at this that I think is key. The key question is, when you compile this Spec# code, what should ILDasm say versus what does it actually say?

Here is what is says:

.method private hidebysig static void  Do(
string modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) s)
cil managed
{
  // Code size       12 (0xc)
  .maxstack  8
  IL_0000:  ldarg.0
  IL_0001:  call       instance int32 [mscorlib]System.String::get_Length()
  IL_0006:  call       void [mscorlib]System.Console::WriteLine(int32)
  IL_000b:  ret
} // end of method Test::Do

The method itself doesn't actually enforce anything, although as we can see, requires s != null causes the compiler to generate CLR Metadata. The folks who developed Spec# ultimately decided that Embedded Contract Languages were the way to go. However, they cite Eiffel and not Sather (a more powerful enhancement of Eiffel that effectively supports automated differential contracts), and the others they cite (Spec#, VCC, SPARK, Dana Xu's work on Haskell) are different from Sather. Sather was also the first to differentiate between Plain Old Assertions and {preconditions, postconditions, invariants}. In Sather, the latter could be used with type contracts to inherit refined types. So I stick with Sather's judgment that "Embedded Contract Languages" equals assertions, not Design By Contract.

To truly get Design By Contract in the Microsoft Research view of the world, you now need mirrors. None of this hodge-podge ccdoc tooling where textual documentation is in charge, or peeking at things with ILDasm or reflector. The need for mirrors calls into question, in general, how Microsft Research so far has viewed (really, ignored) refleciton (IMHO).

I actually also want you to think even a step further. Most examples of Spec# show annotating classes (actual code!), not interfaces (demonstrating true refinement of a specification). This is where you actually see the difference between approaches, because Spec# especially had this problem; if you inherit from a type via "using", then you now have a potential Fragile Base Class problem when you swap out the base class for one in another assembly, because you've now altered the contract.

Postscript: Fixed code formatting June 15th, 2010 so that it wasn't ridiculously wide.

Please, see HOSC.

Especially the oldest paper on it.

Authors there prove equivalence of addition of Church numbers in two encodings (as data and as functions).

This seamless switching has to do with the fact the semantics are consistent. The notation essentially doesn't matter because the semantics model real world phenomena so incredibly well.

Let's flesh this out with an example; Petri nets.

A software engineer does not seamlessly switch between Petri nets and Actors representation of a problem, most notably because of the "limitations" of Petri nets given by Carl Hewitt. The biggest objection of Petri nets is that they are hard to map to physical systems. In this sense, Petri nets are not as useful as Maxwell Equations.

Now THAT is a powerful objection. Everything you said above just doesn't seem like a powerful argument I care about... Sorry.

Lol. What constitutes a powerful argument for you? A long sentence with a lot of references to thoughts which are not your own?

Never mind. You don't have to care about my arguments. They are more of a set of strong opinions than arguments. I think that all arguments which are not proofs are pretty much a waste of time.

I was not trying to sound competitive or even mean. I was simply being very direct. I am very poor at sugar coating things in tasty to digest ways.

What constitutes a powerful argument for you?

Follow this discussion, tracing back over it, and how you and I were communicating, one step at a time. You objected to the comparison of Petri Nets to Maxwell Equations. You called Maxwell Equations "god-given", because they describe basic 'facts' about the physics of the real world using mathematics. I then referenced Hewitt's objection to using Petri Nets to model systems, because like you, Hewitt believes you should strive to come up with a model of a system that mimics the real world.

I think that all arguments which are not proofs are pretty much a waste of time.

An absurd position replied to with reductio ad absurdum: That means the only feedback you will accept on your programming language is a proof that its semantics are inconsistent!

I don't have to care about your arguments, and you don't have to care about my feedback. However, people often criticize me as a practitioner for citing other people's ideas. They tell me it actually weakens my credibility, because I don't have ideas of my own but rather just use the ideas of others in a principled fashion. This criticism is absolutely bizarre, anti-intellectual, and just plain insisting on standing on others' toes instead of others' shoulders.

I read a lot. More than some. I tend to understand very well what I read, because I am committed to understanding it and coming up with practical examples to sketch out its usefulness.

I try to avoid coming up with buzzwords for concepts, and pretend I invented something. What I usually try to do, is when I have an idea for some project, I try to come up with a list of things to describe that idea -- building a huge mind map of the idea. Then I use a ton of search engines and just relentlessly research the hell out of the topic. Sometimes when researching, I'll find a cool paper with a cool idea unrelated to the issue at hand, and I'll save it. It always turns out that 8 months later I end up needing it, anyway.

I also do one other thing. I try to characterize a known solution to a problem, figuring out what buzzwords are used for it, and then type those buzzwords into Google and slap on redneck words like "sucks" to the end of the search. For example, "triggers sucks" or "triggers suck", to find out what programmers think of database triggers and why they dislike them. I also buy lots of books that do design critique, to learn what people feel is a 'good solution' and a 'bad solution'.

Here, in this conversation, I am sharing with you some feedback on what I've seen as a 'bad solution' (Petri nets as a model of real world phenomena) plus the critique (by Carl Hewitt, a programming language designer and computer scientist). If all you can relate back to me is your opinions (and nobody elses), then that's fine. But it does not denigrate the fact I have a wide body of knowledge and apply it regularly, and the massive expense required to acquire that knowledge. -- You can always 'blaze your own trail' instead.

However, "to get something out of nothing, all you need is one principle". Historically, one principle does not show up by blazing one's own trail. Maxwell Equations are a good example, as Maxwell relied on many known principles. His great achievement was showing how when combined they could describe most of the world on a t-shirt.

I think the main reason why both math and physics people look down into CS is the lack of results that capture imagination. Math has Euler formula connecting e and pi, and physics has E=mc^2. The situation would improve when CS generates something as fascinating (and I believe it will).

CS has already come up with such a thing: the P=NP question (intuitively meaning "creativity is expensive"). This question becomes more and more mysterious the more one looks at it. For example, it is just as mysterious and unsolvable in quantum computing and relativistic computing as in mainstream computing technology. The more one looks at it, the more it seems to be a law of nature rather than a mathematical statement. Some people have suggested adding it as a fundamental principle at the same level as Conservation of Energy, something like a "Fourth Law" of thermodynamics. Our universe seems to be built in such a way that creativity requires blood, sweat, and tears.

The lambda calculus, universal Turing machine, and SK combinator calculus aren't enough? The Curry-Howard Isomorphism? The Calculus of Constructions?

I have to suggest that the reason you don't believe CS has generated something as fascinating as e^i*pi + 1 = 0 or e=mc^2 might be because you haven't understood their implications.

Re: comment-60211:

The lambda calculus, universal Turing machine, and SK combinator calculus aren't enough? The Curry-Howard Isomorphism? The Calculus of Constructions?

Those are all results that lie on the math side of the fuzzy border that divides computer science and mathematics proper.

I'd be hard-pressed to define computer science for you but Pеtеr Dеnning gave it a shot. See his summary of the Great Principles of Computing. Nary a mention of Curry-Howard there.

I guess my problem with those "Great Principles of Computing" is that none of them tell me what computing is or how it's done. Feels an awful lot like empty philosophy to me.

The lambda calculus, universal Turing machine, and SK combinator calculus tell us what computing is by describing three ways to do it, all of which have been proven equivalent. Perhaps more importantly, they tell us what the constraints on computation are: what we cannot compute, with any amount of effort.

Similarly, whatever your feelings about the relationship between computation and logic might be, the Curry-Howard Isomorphism establishes that it exists. That's absolutely foundational even if you choose to ignore it completely.

So I'm afraid that "Those are all results that lie on the math side of the fuzzy border that divides computer science and mathematics proper" is mistaken.

Lambda calculus, universal Turing machine, and SK combinators all focus on one in-the-small aspect of computing - essentially, transforming an input string into an output string. If you say that computing = calculation + communication, then you can note this transformation aspect is entirely about 'calculation'.

"Communication" is the aspect that takes into account persistence and state and time, hidden models, hidden agents, demand and observer-effect, software life-cycle (vision, requirements, design, implementation, debugging, deployment, maintenance, extension), concurrency, users, disruption and resilience, security and IA, the source and destiny of information.

A focus on calculations (and algorithms, types, etc. for expressing the calculation) misses what I'd consider the soul of computation science.

We can model communications algorithmically, of course. But any such model will be incomplete and imprecise. Further, unless the model is designed in certain ways - i.e. accounting for open, decentralized, distributed, extensible, scalable, secure, robust, persistent, resilient and disruption-tolerant, live programming - then it will prove ineffective for real world use.

While UTM and Lambda Calculus are important to the history of computing, I'm not convinced they are viable foundations for its future. It is pointless to model communications on a UTM or in Lambda Calculus or with SK combinators, as the resulting models will fail for every relevant attribute.

Communications need a first-class model of their own. And once you account for that communications model, the calculations model will be either subsumed or subordinate. If I were to point to foundational models, my choices would include such things as shared monotonic state, shared destructive state, reactive programming, dataflow, message passing, synchronization and workflow, pluggable architectures, publish/subscribe models, object capability model. UTM and lambda calculus wouldn't even make my list. Rules on the order of E=mc² could include the four conditions of deadlock, the basic physical and logical requirements for communication, the energy motivations for conservative logic.

If anything, the algorithmic (UTM, lambda calculus, SK combinators, et. al.) basis of 'computing' has been hurting us for years, forcing us to fight our way around ineffective and insecure models and architectures for expressing in-the-large communications, open systems composition, life-cycle.

Certainly, calculation is important. But to suggest that calculations, models, results that focus on algorithms or closed systems "lie on the math side of the fuzzy border that divides computer science and mathematics proper" is a fair and reasonable assessment.

...but I'm still going to have to disagree with the conclusion, and my critique of the principles I was offered still stands. That is, my claim is that it's logically incoherent to talk about principles of computer science that say literally nothing about how computation is done.

dmbarbour: If I were to point to foundational models, my choices would include such things as shared monotonic state, shared destructive state, reactive programming, dataflow, message passing, synchronization and workflow, pluggable architectures, publish/subscribe models, object capability model. UTM and lambda calculus wouldn't even make my list.

Each and every one of those is expressible in terms of one of the lambda calculus, UTM, and/or SK calculus, and in the case of the object-capability security model, I'm hard pressed to figure out how you'd say anything meaningful about it without reference to the lambda calculus in particular, as exemplified by Jonathan Rees' "A Security Kernel Based on the Lambda Calculus".

Now, it may be that you just mean that, e.g. the original untyped lambda calculus etc. may be insufficient. I don't disagree with that. But that's nevertheless how we got to, e.g. the quantum lambda calculus, and now we're closer to the realm in which we can talk meaningfully about the ways in which "Communications need a first-class model of their own. And once you account for that communications model, the calculations model will be either subsumed or subordinate." My assertion is only that the result will be a calculus that relates to the lambda calculus, UTM, and/or SK calculus in a way that's isomorphic to how, e.g. general relativity relates to Newtonian mechanics, or indeed quantum mechanics relates to Newtonian mechanics (cf. Schrödinger's equation and the Hamilton-Jacobi equation).

But to say "UTM and lambda calculus wouldn't even make my list" seems, frankly, trivially misguided.

Each and every one of those [communications models] is expressible in terms of one of the lambda calculus, UTM, and/or SK calculus

I disagree. You cannot express open and evolving systems within those models [λ-calculus, UTM, SK calculus], all of which are closed by their definitions, so you cannot faithfully 'express' those models.

Further, any attempt to adapt a model so that it can operate in an open system should be understood as developing a new model. Actors model is not the lambda calculus, despite having some historical origins in it.

In practice, in reality, on the computer science side of that "fuzzy border that divides computer science and mathematics", the communications and concurrency and security models are fundamental. UTM, lambda calculus, and SK combinators are irrelevant. (And, yes, I'm speaking of the original models.)

If you want to "say literally nothing about how computation is done", then go ahead and talk about UTM and lambda calculus and SK combinators... and do the usual hand-waving song and dance that completely elides the real concerns for how data meets code in the first place, how they are deployed and maintained, how computations compose and interact.

Well, I'll admit the 'literally nothing' is unfair. Algorithms and calculation are an important part of computation. But to say they are "how computation is done [...] seems, frankly, trivially misguided". After all, no computation would happen at all with the lambda calculus alone.

Anyhow, I already responded to much of this within the earlier comment, at: "We can model communications algorithmically, of course. But..."

My assertion is only that the result will be a calculus that relates to the lambda calculus, UTM, and/or SK calculus [...] But to say "UTM and lambda calculus wouldn't even make my list" seems, frankly, trivially misguided.

I'm not convinced. Who's to say that, a hundred years from now, our computation systems won't have a stronger foundation in term-graph rewriting, conservative logics, cellular automata (reactive state machines), Petri nets, or any of dozens of other 'equivalent' models of computation old or new?

UTM is already a historical footnote - and perhaps started its life that way: its most direct and diligent implementations are called 'Esoteric'. Lambda calculus is still holding strong as the basis for many languages, but lambda calculus is based on term substitution; term-graph rewriting and logic programming are both powerful competitors with regards to the 'pure' lambda calculus model. None of the three models you name are related to concurrent constraint programming or declarative concurrency, and the relationship to message-passing is mostly by historical lineage.

I don't point at the Rutherford model of atoms as foundational in chemistry or physics, despite the fact that it makes many good and accurate predictions, is an important part of our history, influenced modern atomic models and vernacular, and resulted in a lot of cool logos for physics and chemistry research. In that same sense, I don't point at 'lambda calculus' as foundational in computation science, despite the fact that it is useful, is an important part of our history, has influenced a wide variety of modern models and languages, and the has resulted in a lot of cool logos for Programming Languages Weblogs and research communities.

A historical relationship must not be a sufficient condition for modern theoretical foundations, lest we allow absurd arguments that Organon is foundational to modern atomic theory and computation science...

I'm hard pressed to figure out how you'd say anything meaningful about object-capability security model without reference to the lambda calculus.

A pure lambda calculus trivializes the object-capability model; there's simply no point in thinking about capabilities if you don't have hidden-model communications effects.

And the impure lambda calculus is unnecessary for object-capability model, despite being useful for offering concrete examples and explanations. That is, there exists an infinite variety of non-lambda-calculus models for which object-capability model is useful and meaningful.

If you believe lambda-calculus is necessary for object-capability model, then you've misunderstood object-capability model, which is really about rules for communications connectivity for an evolving communications graph in an open system (involving interaction with untrusted code).

It's logically incoherent to talk about principles of computer science that say literally nothing about how computation is done

To be fair, you must recognize that you were reading the headlines/highlights of that linked paper, and not the actual paper.

The author of that list believes (as I do, as Carl Hewitt and Alan Kay and Karl Fant do) that computation sciences started off on the wrong side of the bed by understanding computation in terms of in-the-small algorithms and calculations rather than in terms of in-the-large communications and information processing.

The 'goal' we strive for is to produce an executable model that is "as simple as possible, but" that will properly capture all aspects of computation, including communications and attendant interests (software life cycle, security, concurrency, disruption, resource conservation, etc.) while allowing one to understand interesting properties of the concrete systems so modeled.

Naturally, we only learn that a model is flawed in hindsight. The search space for computation models is ridiculously large, and there are emergent ramifications for what may seem initially to be minute decisions. Understanding the composition and expression properties and effectiveness of any promising model takes blood, sweat, tears, gummi-bears, and much loss of hair. Nobody is to blame for a misstep.

I have come to believe that message passing models are one such misstep, and shared state communications is certainly another. I'm recently pursuing an alternative model, RDP. I'm certain I'll make my own missteps - I've been retracing steps and trying different things for eight years now, and I know that RDP (despite its many virtues relative to message-passing and shared-state models) still fails to model resource conservation.

I'll take a look at the 'quantum lambda calculus'. Thanks for the link.

...and I didn't articulate the important aspects of my point well.

David Deutsch's claim, which is nicely summarized in this interview, is that quantum information theory and quantum computation are information theory and computation, which is to say that their formulation is a generalization of that which came before them, historically. I tried to allude to this, poorly, by saying that I expect a unified computation/communication framework to be isomorphic to the historical mathematical logical foundations as quantum mechanics is to Newtonian mechanics.

So I don't think we really disagree on what the ultimate goal is. We might disagree slightly on how "close," in some sense, the result is likely to be to the things that I think of as foundational to computer science today, but really, I think that's a matter of relatively little import. The key point is that we have some signposts.

dmbarbour: To be fair, you must recognize that you were reading the headlines/highlights of that linked paper, and not the actual paper.

Sure, but they were labeled as the principles. This is a general problem that I have with attempts to declare something other than LC, UTM and/or SK "principles of computer science:" if they make no reference to any mathematical/logical expression, I'm not prepared to read the supporting material, because the mathematical/logical expression is where the concision and precision is found. That is: if there's no math in the summary, I don't trust that I'll find it anywhere else, especially considering that you can express beta reduction in a paragraph. And if there's no math, well, what's being said is not only not foundational, it's nonsense.

I guess, for me, it comes down to this: computation is a physical process because everything is a physical process. We describe physical processes mathematically; computation is no exception. It's true that our mathematical descriptions of computation have historically left out much of the physics of information (but not all, cf. Reed-Solomon error-correcting codes, etc.) but that is being addressed. It's just being addressed by extension and refinement, not by overturning what came before. It's not possible to overturn what came before, any more than it's possible to overturn Newtonian mechanics.

It's not possible to overturn what came before, any more than it's possible to overturn Newtonian mechanics.

Here's a different spin on that same argument: "It's not possible to overturn what came before, any more than it's possible to overturn the Ptolemaic system with its epicyclic orbits."

I guess the question becomes: at what point does replacing or tweaking a model qualify as overturning it?

As I understand it, models can be killed by Occam's razor, neglect, and various social processes.

Newtonian mechanics holds on, despite known inaccuracies under some extreme conditions, because it is 'good enough' for day to day work and is relatively simple. And it will probably continue to do so long past my death. But who knows... perhaps it will be replaced by something even simpler and more accurate? Long histories show such events happening repeatedly, and I'm not arrogant enough to believe our century will become an exception... especially not for a field as young as computation science.

It's just being addressed by extension and refinement, not by overturning what came before.

Beware the "just".

It is my experience that extending models tends to increase their complexity, thus making them more vulnerable to Occam's razor.

Further, I have already mentioned emergent effects that can arise from seemingly innocent tweaks. To add imperative side-effects to the lambda calculus is to annul almost every interesting property you could observe with respect to studying modular systems modeled in a pure lambda calculus. That is, an extension to a model may well and truly 'overturn' the conclusions one can make in that model.

This is no less true of physical models. You do not 'just' extend and refine Newtonian mechanics. Every extension or refinement requires much 'just'ification.

Rather than extending models, it is safer to embed or layer them. But, even in that case, you may discover said embedded model is a redundant hanger-on that isn't necessary or that may at least be reduced greatly. Further, you'll still be increasing their complexity. My development of RDP came by simplifying a layered model that included both message-passing and FRP-like data pipes.

Computation is a physical process because everything is a physical process.

With that much, I agree. But the statement is incomplete. Computation is also a social process because it exists in a social framework.

To neglect such a relevant aspect is to prepare for failure. You cannot drive a car on physics alone. You cannot survive just by understanding your internal biology.

In addition to its physical aspects, a computation must be modeled as part of a larger social and economic system.

We describe physical processes mathematically; computation is no exception.

How absurd! How patently untrue!

We do not describe most physical processes mathematically - especially not when said description is to be executable. Read the back of a shampoo bottle, cook some recipes, study a surgical process, read a manual for replacing the oil of your vehicle, and then teach me to smoke.

Descriptions of physical processes are often an even mix of declarative and operational, and neither of those aspects is remarkably 'mathematical'. What is especially 'mathematical' about a plan for one vehicle to pass another without violating municipal law or collision?

We use mathematics for predictive modeling, and we use mathematics to transform data to prepare for input to the models, and we use predictive models to support planning and control, and then we repeat the whole process for the first goal of the selected plan until we reach executable primitives... and so you might say we usefully apply a lot of mathematics. And you'd be right!

But nowhere in that chain do we mathematically describe an executable physical process.

but they were labeled as the principles. This is a general problem that I have with attempts to declare something other than LC, UTM and/or SK "principles of computer science"

UTM, LC, and SK are not 'principles' any more than Newtonian mechanics is a principle. A better word for those would be 'models'. Principles, as I understand the word, describe things common across models, such as conservation of energy in a closed system, Rice's theorem, Incompleteness theorem, and the fact that you cannot write a self interpreter within a terminating language.

Equations and relationships can only be expressed within a model, and even then may be unclear if the model for expression is incomplete or inadequate. Expressing various communications 'principles' with lambda-calculus expressions wouldn't be any easier than expressing chemical processes in Newtonian mechanics.

I suspect attempting to explain a model and the equations at the headlines/highlights page would be a poor strategic decision even if the equations were available. Hyperlinks would be nice, though.

However, I'm not trying to defend the articles. I'll readily agree that most of Denning's 'principles' are questionably even that. the points on AI sound more like personal definitions, and the point on 'thrashing', while reasonable as an empirical observation, is at the very least worded poorly for use as a principle). I've not done more than skim a few of the pages, and it strikes me as somewhat hand-wavy.

Rather, I'm disagreeing with your conclusions: arguing Lambda Calculus to be a 'principle' strikes me as a category error. (If LC is a principle, then why not every computation model?) And, even if every point had a firm mathematical foundation (which isn't true, but even if) listing the equations would detract from the high-level summaries list of headers.

dmbarbour, quoting me: "We describe physical processes mathematically; computation is no exception."

dmbarbour: How absurd! How patently untrue!

Um, no. Neither absurd nor untrue. Note that I didn't say that we only describe physical processes mathematically. Rather, the point is precisely that those descriptions are foundational: any useful abstraction of the description of the process (of which, to be perfectly clear, there are many) can nevertheless be expressed in terms of mathematics. That's what's meant by "foundational."

dmbarbour: Read the back of a shampoo bottle...

Shampoo -> biology -> chemistry -> physics -> mathematics.

dmbarbour: cook some recipes...

Cooking -> nutrition -> food chemistry -> physics -> mathematics.

dmbarbour: study a surgical process...

surgery -> physiology -> biology -> chemistry -> physics -> mathematics.

dmbarbour: read a manual for replacing the oil of your vehicle...

Auto maintenance -> mechanics -> chemistry -> physics -> mathematics.

dmbarbour: What is especially 'mathematical' about a plan for one vehicle to pass another without violating municipal law or collision?

You're joking, right? Let's check in with the developers of the "Grand Theft Auto" franchise.

The Great Crux is that you're rather obviously talking about abstractions on top of mathematical logic and then claiming that the mathematical logic isn't foundational just because you choose not to examine the abstractions at that level of detail. To bring this back home, by all means, come up with a successor to FRP or whatever you would like to do. Just be aware that, if its description has predictive and explanatory power, it will be provably isomorphic to the lambda calculus, UTM, and SK combinator calculus.

Re: comment-60238:

… by all means, come up with a successor to FRP or whatever you would like to do. Just be aware that, if its description has predictive and explanatory power, it will be provably isomorphic to the lambda calculus, UTM, and SK combinator calculus.

Is that provably isomorphic or probably isomorphic?

What about a MacBook Air orbiting a black hole in a Malament-Hogarth spacetime? (Kidding.)

el-vadimo: Is that provably isomorphic or probably isomorphic?

This is actually an excellent question, serious or otherwise! My "mathematical chauvinism" :-) is very much informed, as I've written before, by the Laplacian-Coxian-Jaynesian perspective on probability, which is to say as an extension of logic, as described here, and also as informed by New Axioms for Rigorous Bayesian Probability, which resolves the observation that Cox's "theorem" wasn't actually axiomatized and, in fact, a counterexample was found by Halpern.

So from that point of view, the difference between "provably" and "probably" comes solely down to how much information we have a priori. If we have enough, it's "provably." If we don't, it's "probably," but, critically, as we gain more information, "probably" becomes "provably," in the literal sense that the sum and product rules of Bayesian probability reduce to modus ponens when probabilities go to 1.0.

Perhaps this helps provide some basis for understanding why I take the tack that I do. It's not that I don't believe higher levels of abstraction are useful, even important: I do. And it's not that I think everything we want to reason about is known well enough to be amenable to reasoning using, e.g. even higher-order logic: I don't. All I believe is that any theory with predictive and explanatory power can be expressed in probability-as-logic. Sometimes it's practical to do so, as current machine learning research reveals, and sometimes it isn't. But the connection is always there, and helpful to be mindful of whether we exploit it deliberately or not.

I'm sorry, I can't take your argument seriously.

X -> blah -> blah -> physics -> mathematics

And therefore everything can be modeled mathematically? Or is modeled mathematically? These arrows have an interesting character. I'd be interested in seeing what happens if I write:

mathematics -> ink

So therefore everything in the universe can be modeled with ink? Because ink can be used to encode mathematics, after all. Or mathematics can be modeled with a series of clicks and whizzes--therefore clicks and whizzes are foundational?

If you want to string arrows together all day in order to prove that everything is mathematics, be my guest. I'm interested in the mathematical description you can provide of shampoo.

Re: comment-60245:

X → blah → blah → physics → mathematics

And therefore everything can be modeled mathematically?

Paul knows very well that hot bakery items cannot be modeled mathematically. (Not in California, anyway.)

And just so I don't forget…    Re: comment-60242:

My “mathematical chauvinism” :-) is very much informed

… the above is in reference to this post on the SEMAT thread.

el-vadimo: Paul knows very well that hot bakery items cannot be modeled mathematically. (Not in California, anyway.)

I know no such thing. What I do know is that legislative language is maddeningly vague. Nevertheless, people implement systems that adhere to it well enough for practical purposes (i.e. maximizing profit/minimizing non-compliance costs) all the time, and that process necessarily involves coming up with a formalization of the vague legislative language. If you doubt this, consider the legislative verbiage around the regulations of, e.g. air travel, and then consider the software involved in analyzing sensor data, tracking maintenance activities, fuel consumption and emissions, required ground facilities, required work/rest schedules for crew, etc. Positing that human language is vague tells us exactly nothing about whether something can be modeled mathematically or not.

...by which I only (some "only") mean that mathematics is the language that humanity has created for the purpose of being concise and precise in describing the world. As I wrote, there are many useful levels of abstraction well above the most fundamental mathematical one, but claims that they are themselves foundational are false.

Ben L.Titzer: I'm interested in the mathematical description you can provide of shampoo.

I have to say the same thing I said to dmbarbour: you're joking, right? By all means, please visit a shampoo manufacturer and talk to their chemists and ask them about, to name just one obvious example, the toxicity studies that they are required to do on their products.

Claims that there exists a "fundamental mathematical one" strikes me as wishful thinking, and inaccurate in practice.

Even for toxicity studies.

While I may not be an "expert" in this area, I am probably the most knowledgable person here on LtU with regard to current techniques used by chemists to determine toxicity of chemicals to humans -- and the most qualified to dismiss your "you're joking, right?" remarks. After all, I worked two summers for a PNAS fellow who pioneered nuclear imaging.

Bottom line: Determining the toxicity of every compound that could possibly be synthesized in the universe would require smashing together more atoms than exist in the universe. For this reason, we might build a predictive model that says "due to other examples of chemical compounds with similar substructures to this one, we think the compound you're thinking of developing will result in paralysis in humans. Here is a list of research papers in chemistry that we used to determine this..." This approximates how data mining tools at Glaxo-Smith-Kline probably work. They also are probably more advanced, to the point of suggesting you could do something else to achieve the same effect. And in the future, I suspect they'll even suggest end-to-end engineering for a compound, automatically. All you need is (good) data and the right search/mining tools.

But companies like GSK lose the art of chemistry in the process of all this automation. That art is best exhibited by how my mentors could just look at a compound and discuss it, without software at their disposal, and get a good idea for how they can synthesize it, if at all. For example, the legendary synthesis of Vitamin B-12 (which is constructible only with the help of bacteria), the publishing of which is a career-defining synth paper in chemistry, is really non mathematical in a computational sense I think you hope for.

[Side note: That sort of engineering is probably why at most pharma companies the hottest positions are actually engineering positions, not chemist positions -- all (Asian) chemists go (back) to Asia after they get their education in the US at the US's great universities, because US companies don't pay chemists squat compared to engineers. Having a Ph.D. in chemistry for instance can actually make you overqualified for most US pharmaceutical positions, because you are too theoretical, too non-applied, too pricey (you've got to pay back Harvard somehow). "Process engineers" in pharma companies are one of the hottest jobs in America right now, because you have to be (a) ridiculously smart (b) good communicator (c) good at seeing how to automate things and refine things (d) not already in consulting :)]

Given what I've just described, I still agree with Ben, your -> has mysterious powers.

You're singing from my songbook, which tells me I'm faring poorly at making my point.

This approximates how data mining tools at Glaxo-Smith-Kline probably work. They also are probably more advanced, to the point of suggesting you could do something else to achieve the same effect. And in the future, I suspect they'll even suggest end-to-end engineering for a compound, automatically. All you need is (good) data and the right search/mining tools.

Right. My claim is that data and search/mining tools are mathematical. Is this actually controversial somehow?

For example, the legendary synthesis of Vitamin B-12 (which is constructible only with the help of bacteria), the publishing of which is a career-defining synth paper in chemistry, is really non mathematical in a computational sense I think you hope for.

I think the word "computational" here is key. That is, I think people think that I'm saying something really ridiculous, like that you can describe the entire multiverse in terms of first-order logic, or something very much along those lines. I'm not. I'm saying that the most foundational description of everything that we have is physics; that the most concise and precise way we have of talking about physics is mathematically; that any description of physical processes, including computation, that has predictive and explanatory power can be elucidated in mathematical terms; and that very often doing so extends the reach of the model thus arrived at. This is proving particularly trenchant precisely in domains such as yours (as you described), and really in more applications than I can count: machine learning is teh new hawtness, and is very definitely part of what I'm referring to in my comments.

Z-Bo: Given what I've just described, I still agree with Ben, your -> has mysterious powers.

They're not mysterious; they're just hard, for exactly the reasons you've described.

None of this is to suggest that human intuition doesn't precede the automation, by the way! On the contrary; we fans of E.T. Jaynes will be the first to tell you that any Bayesian process needs its priors. :-)

As I wrote, there are many useful levels of abstraction well above the most fundamental mathematical one, but claims that they are themselves foundational are false.

Many? In one--arguably very real--sense, there are only two levels of abstraction that actually matter: None at all, and hand-waving vagueness that relies on the audience to figure out what you probably meant. Anything that appears to be in between is usually reducible, by some series of steps, to a minimal core of hand-waving. Mathematics, then, consists of various tools for constructing complex ideas out of simpler ones, without introducing more hand-waving than is already present.

Unfortunately, machines don't do very well with hand-waving. The fundamental task of software development is taking a large hand-wavy task, reducing it to a small hand-wavy core, and then fudging things a bit to produce something with virtually no hand-waving whatsoever that solves approximately the same problem, while hoping nobody notices the difference.

So, it's all well and good to note that many things are fantastically difficult to describe given only mathematics and the quantity of hand-waving allowed by a computer program. That's certainly true! But the moment one introduces additional hand-waving, one has left the realm of meaningful computation, by relying on some other human to interpret the vague parts.

I may be overly skeptical--perhaps due to having little academic background--but I find myself suspicious of attempts to avoid mathematical formalisms regarding computation. At the end of the day, I'm a programmer, and I have to explain things to these stupid machines in terms they can understand, so I don't have much use for informal "descriptions".

In short, I'd like to see any workable description of shampoo or whatever--mathematical or otherwise--because as far as I'm concerned, if it doesn't compile, it's not a description at all, just yet another vague, unclear project spec, and unless I'm getting paid for it that's just wasting my time.

The fundamental task of software development is taking a large hand-wavy task, reducing it to a small hand-wavy core, and then fudging things a bit to produce something with virtually no hand-waving whatsoever that solves approximately the same problem, while hoping nobody notices the difference.

Wonderfully stated. :-)

any workable description of shampoo or whatever

Try: lather, rinse, repeat until out of shampoo...

Those would be the instructions on the back of the bottle. You'll need to find different instructions if you work for a shampoo factory.

At the end of the day, I'm a programmer, and I have to explain things to these stupid machines in terms they can understand, so I don't have much use for informal "descriptions".

Seriously? I suspect you'd be out of work if you were always given formal descriptions. At the end of the day, I'm also a programmer, and my job is to bridge the gap between informal hand-wavy moving-goalpost requirements... and an executable more-or-less hand-wavy "description".

Executable hand-waving = heuristics, configurable defaults, and prototypes.

Try: lather, rinse, repeat until out of shampoo...

Hm, the base case is a nice touch, there--definite improvement over the usual infinitely recursive version!

Still slightly lacking in detail, though. Bit of a leap from that to, say, programming a robot to wash someone's hair.

Seriously? I suspect you'd be out of work if you were always given formal descriptions. At the end of the day, I'm also a programmer, and my job is to bridge the gap between informal hand-wavy moving-goalpost requirements... and an executable more-or-less hand-wavy "description".

Well, that was my point, albeit expressed poorly--that's what I get paid for. The corollary being, if I'm not getting paid for it, I don't want to deal with it! Nice, clean, mathematical formalisms make my life easier, because they let me build fancier things with less hand-waving. Deciphering hand-waving? That sounds like work.

But the original idea was simply that, if something is not sufficiently precise such that it can be compiled, it has no relevance to fundamental principles of computation, on pain of broadening the definition of such to an absurd degree. In practice, this seems to always lead back to mathematical formalisms, and something equivalent to all the usual stuff.

those descriptions are foundational: any useful abstraction of the description of the process (of which, to be perfectly clear, there are many) can nevertheless be expressed in terms of mathematics. That's what's meant by "foundational."

So the logical foundation is always mathematical because it can (allegedly, potentially) be mathematical?

The Great Crux is that you're rather obviously talking about abstractions on top of mathematical logic and then claiming that the mathematical logic isn't foundational just because you choose not to examine the abstractions at that level of detail.

No, I'm saying the "Mathematical logic" isn't there to begin with, entertaining confabulation notwithstanding.

We fail to examine abstractions at given levels of detail because we lack information, we lack patience, we lack accurate or precise models, and we often lack computational resources. And this will always be the case.

The Great Crux is that you're rather obviously talking about an application of mathematical logic where, historically, none was ever applied. Anything you deduce from such historical (non-)applications of mathematics is, by nature, vacuous. Might as well talk about all the elves, tooth fairies, and pink invisible unicorns you used in developing those 'lather once rinse twice' instructions on the back of the shampoo bottle, or in choosing the shampoo's 'fresh' scent.

To bring this back home, by all means, come up with a successor to FRP or whatever you would like to do. Just be aware that, if its description has predictive and explanatory power, it will be provably isomorphic to the lambda calculus, UTM, and SK combinator calculus.

I'm assuming you constrain yourself to homomorphisms that maintain property of functional equivalence (same string out for a string input) across the transform, and are asserting that you'll additionally maintain static (description-time) properties of "predictive and explanatory power" for various useful characteristics (i.e. for analysis of safety, correctness and bug-hunting, functional equivalence, local termination, idempotence, parallelism, partial-evaluation, dead-code elimination, liveness analysis).

If my understanding of your words is accurate, then you are mistaken. Turing equivalence says that you can describe the same set of closed-system computable functions. This is not the same as maintaining predictive and explanatory power from the function's description. Even for closed models, you cannot assume you'll maintain predictive or explanatory features regarding type-safety, termination or progress, observational equivalence. Nor is it trivial to claim an isomorphism: even though you might produce a homomorphism in each direction, f : L -> M and g : M -> L, it is non-trivial to obtain g = f-1 - not even for closed systems.

All the most interesting artifacts of Computer Science and Software Engineering involve open systems and hidden models. For these systems, one must make predictions and explanations with regards to such properties as extensibility, concurrency, deadlock or livelock, security, performance, deployment, maintenance and upgrade, disruption tolerance, resilience, robustness, well-timing properties, and safety; further, these predictions must involve local reasoning and apply across composition. Reasoning about observational or functional equivalence is relevant for optimizations, but is only one of many interesting properties worthy of prediction and explanation.

I do not believe you can produce a homomorphism g : M -> L from an open system with hidden models to a closed one such as lambda calculus. The best you can do is formulate an incomplete and incorrect axiomatization (model) of the open system within the closed system. Naturally, a closed and incomplete model will not be functionally equivalent to the open system with its hidden models.

Ultimately, I do not see your 'mathematics' and 'isomorphism' arguments as valid even for models of closed systems, much less for models of open systems. Even if the physical world has mathematical explanations, we lack access to that information - doubly so given the latencies between describing executable physical processes and executing them.

Our 'logical foundation' is whatever logic we actually use to make predictions, decisions, conclusions, whether that be Bayesian probability, fuzzy logic, paranoid delusion, Aristotle's Organon, or a faith and belief system - not all of these are especially mathematical, and not all descriptions of physical processes reduce to physics.

There's a lot of good stuff here, and I can only take it as a measure of how much I don't understand of what you mean, because I find entire paragraphs of your post completely contradictory, by which I mean that I completely agree with some and completely disagree with others. :-)

To give just one example, I completely agree with this:

We fail to examine abstractions at given levels of detail because we lack information, we lack patience, we lack accurate or precise models, and we often lack computational resources. And this will always be the case.

But this...

No, I'm saying the "Mathematical logic" isn't there to begin with, entertaining confabulation notwithstanding.

...seems obtuse to the point of childishness. You aren't seriously trying to say that the entirety of mathematical development from the ancient Greeks to the present didn't happen, are you? I'm satisfied, given your reference to homomorphisms etc. that this isn't the case, but I'm afraid that that just leaves me feeling that this comment is opaque, at best.

Likewise this:

The Great Crux is that you're rather obviously talking about an application of mathematical logic where, historically, none was ever applied. Anything you deduce from such historical (non-)applications of mathematics is, by nature, vacuous.

I'll be quite sure to tell the entire scientific community from, to be conservative, the 17th century on, that none of them ever applied mathematical logic to their endeavors. :-) More seriously, I have to tell you, in the strongest terms possible, that referring to the mathematical logical analysis of entire scientific domains of inquiry throughout history as "vacuous" manages to be both completely fallacious and unbelievably offensive at the same time. You personally might not engage in such endeavors; you personally might not choose to pursue their results; you personally might not find these processes and descriptions interesting or compelling (although, once again, you make comments elsewhere that lead me to believe this can't be the case). They nevertheless exist and have made it possible, to name just the most obvious example, to have this conversation in this medium.

With that said, on to more fruitful points:

Ultimately, I do not see your 'mathematics' and 'isomorphism' arguments as valid even for models of closed systems, much less for models of open systems. Even if the physical world has mathematical explanations, we lack access to that information - doubly so given the latencies between describing executable physical processes and executing them.

Another point that I wholeheartedly agree with. I merely frame this in terms of the Many-Histories Interpretation of quantum mechanics... which happens to have a mathematical model with tremendous predictive and explanatory power. And quantum computing is moving the "we lack access to that information" ball forward day by day.

In summary:

Our 'logical foundation' is whatever logic we actually use to make predictions, decisions, conclusions, whether that be Bayesian probability, fuzzy logic, paranoid delusion, Aristotle's Organon, or a faith and belief system - not all of these are especially mathematical...

Completely agreed.

...not all descriptions of physical processes reduce to physics.

Completely disagreed.

Mathematical models exist inside the mathematician. They reflect reality. They are not reality. The same is true of physics, chemistry, and biology. The map is not the territory.

I suspect you believe otherwise. The 'universe as a computation' model appeals to you. You feel: reality is a computation, the qbit is the true atom of our universe, and the answer is 42. I must say, this concept appeals to me as well, but I reject it as axiomatic. This difference is a likely 'root cause' of our disagreement. While holding this belief, you understand only half of what I say - and the other half produces cognitive dissonance.

To me, the position that reality is mathematical is wishful thinking at best, and vacuous nonsense at worst. Even assuming a computation describing reality exists, we'll never have access to it in our models. That computation will never be part of our logic.

And, because abstractions are properties of the observers, and mathematical models are features of the mathematicians, there is no such thing as a 'fundamental mathematical abstraction'.

I'll be quite sure to tell the entire scientific community from, to be conservative, the 17th century on, that none of them ever applied mathematical logic to their endeavors. :-)

Sure, they used mathematical logic. But it was never fundamental.

More seriously, I have to tell you, in the strongest terms possible, that referring to the mathematical logical analysis of entire scientific domains of inquiry throughout history as "vacuous" manages to be both completely fallacious and unbelievably offensive at the same time.

I'm sure you can find stronger terms than that. Try harder. >;^)

Anyhow, you misunderstand my assertions. Scientific models are sometimes mathematical. That does not make them fundamental. You said: "you're rather obviously talking about abstractions on top of mathematical logic", and that's untrue. I'm talking about abstractions. On top of what? The answer certainly is not "mathematical logic". If I were to answer, it would be: on top of observations and an entirely non-mathematical assumption that future observations can be predicted from past or present observations.

It is apocryphal to assert that a human's abstractions are on top of "mathematical logic" in cases where no mathematics were actually used in said "logic". (And, yes, "logic" does need the air-quotes with respect to all humans some of the time and some humans all of the time.)

I merely frame this in terms of the Many-Histories Interpretation of quantum mechanics... which happens to have a mathematical model with tremendous predictive and explanatory power.

The Many Histories interpretation does appeal to me: it (for better or worse) is how I grokked the interference patterns for diffraction of single photons. Nonetheless, it is an interpretation. It exists in my head. Other than the extent to which my head is part of reality, that interpretation is not reality.

I must say, I was unaware that this interpretation has any predictive power. I understood it to be strictly an interpretation of results in the framework of the quantum models. A bit like "Zeus did it", but with quantum waveforms instead of lightning bolts.

Quantum computing is moving the "we lack access to that information" ball forward day by day.

One of quantum computing's larger contributions has always been telling us just how little we know.

...not all descriptions of physical processes reduce to physics.

Completely disagreed.

Go talk to some children. Then go talk to some adults. See how long you continue to completely disagree.

The Many Histories interpretation does appeal to me. It was how I grokked the interference patterns for diffraction of single photons. Nonetheless, that is an interpretation. It exists in my head. Other than the extent to which my head is part of reality, the model is not reality.

Fair enough. My question is, does it make any sense to talk about fundamental models that:

1. Add no explanatory or predictive power over the MHI, General Relativity, and Standard Particle Model of physics.
2. Can be reduced to the above.
3. Are even more subject to overinterpretation than mathematics is. :-)

One of quantum computing's larger contributions has always been telling us just how little we know.

And an even larger one has been to demonstrate that some of our models have even greater predictive and explanatory power than we realized when we formulated them, and to put them to use, which is the ultimate measure of progress and, crucially, the validity of the model, whether or not the map is the territory (a position that I really don't care about one way or the other, as long as the map helps me get where I'm going).

Go talk to some children.

The fact that children are unaware of the math and physics behind what they do tells me precisely nothing about the math and physics that underlie everything that they do--including their sheer existence.

does it make any sense to talk about fundamental models [...]

No. It does not make sense to talk about "fundamental models."

some of our models have even greater predictive and explanatory power than we realized when we formulated them, and to put them to use, which is the ultimate measure of progress and, crucially, the validity of the model

Agreed.

The fact that children are unaware of the math and physics behind what they do tells me precisely nothing about the math and physics that underlie everything that they do

Nevertheless, it will beat in a point I've made several times: that very few descriptions of physical processes reduce to what we understand as 'physics'. I've been trying to make that point clear to you, yet it seems you trivialize your position by positing: "but descriptions that don't reduce to physics don't count!". Alternatively, you trivialize math and physics by suggesting a mere relationship is effectively a reduction.

We are all still children. We have models in our heads of what reality is. For the more nerdy among us, those models happen to be heavily mathematical. We know enough to create some nifty toys, and guns, and bombs. There remains a significant gap in our mental models when it comes to understanding politics, economies, and women.

whether or not the map is the territory (a position that I really don't care about one way or the other, as long as the map helps me get where I'm going)

Then allow Occam's razor to eliminate the unnecessary assumption: you do not need to assume the map is the territory. So kill the assumption. The belief that physics is anything other than a model reflecting some aspects of reality is inessential to the validity of the model.

The difference in view is relevant to the human, important for maintaining an open mind. You speak of the "math and physics that underlie everything [we] do" because you believe that physics is more than a model. If you truly embrace the "as long as the map helps me get where I'm going" philosophy, then physics is just one more model - one that is good for making certain predictions, not so good for others.

...and I think we're so far off topic at this point that I'll end it here, but:

Alternatively, you trivialize physics by suggesting a mere relationship is effectively a reduction.

I can see why you would think that, but it's actually not the case. My entire point is that the value of reductionism (whether in science generally or PLT, to try to bring this back home) lies precisely in identifying the building blocks that we can indeed use to synthesize (compose?) something new.

The belief that physics is anything other than a model reflecting some aspects of reality is inessential to the validity of the model.

We don't disagree on this. If we actually disagree on anything, it might only actually be what constitutes a minimal sufficient set of rules/properties, whether you think of these as described mathematically or not. That is, I'm happy with physics "just being a model," insofar as it seems to be minimally sufficient.

There remains a significant gap in our mental models when it comes to understanding politics, economies, and women.

Of course. Nothing I've said suggests otherwise.

physics is just one more model - one that is good for making certain predictions, not so good for others.

That's exactly what I mean when I say that there are many abstractions on top of math and physics that are useful.

Again, trying to bring this home: we're supposed to be discussing programming in the large, right? So we've spilled a lot of virtual ink on philosophy. What's your one-paragraph executive summary as to why PLT/mathematical logic isn't the right framework for accomplishing (whatever we may mean by that) programming in the large?

physics is just one more model - one that is good for making certain predictions, not so good for others.

That's exactly what I mean when I say that there are many abstractions on top of math and physics that are useful.

Huh? To say "physics is just one more model" is not to say "the other useful models are on top of math and physics". So I'm not seeing the 'exactly what you mean' part. Maybe if I cross my eyes and bend my mind for a while...

the value of reductionism (whether in science generally or PLT, to try to bring this back home) lies precisely in identifying the building blocks that we can indeed use to synthesize (compose?) something new.

There is a cost to accompany the value of the reductionism philosophy, oft in the form of magnificent hand-waving, premature generalizations, and towering monuments to geekdom. I recall spending a few hours wondering how many-histories interpretation relates to throwing a baseball: is it possible that, in some history, the baseball is propelled by unlikely circumstances all the way around the world? And moving baseball is also a waveform... so what does baseball diffraction look like? How do thrown-baseball histories interfere with one another?

The notion of identifying a basic set of building blocks for composing software, and of allowing the choice of these building blocks be influenced by what we understand of physics, are both reasonable - perhaps even necessary for developing scalable software systems.

Yet even limiting ourselves to physics-influenced software primitives leaves a frightfully wide language-design space.

What's your one-paragraph executive summary as to why PLT/mathematical logic isn't the right framework for accomplishing (whatever we may mean by that) programming in the large?

Programming-in-the-large is a primarily social phenomenon. The most relevant concerns are development, deployment, integration, configuration, maintenance, security, trade, and more - in general, software life-cycle, composition, and local reasoning in an open system. Due to various security, trade, deployment, and configuration concerns, hidden models are fundamental to programming-in-the-large. Due to nature of social relationships, interaction with these will be partially predictable: convention, protocol. Nonetheless, because they exist in an open system, these hidden models will generally be both concurrent (varying independently of one's own interactions) and mathematically irreducible.

Models of physics, models of social interactions - both are powerful bases for developing languages with effective in-the-large properties (ranging from scalability and performance to coordinating diverse interests, cooperating with mutual distrust, trade, and market integration). But none of our models is 'foundational' - through history, and in terms of predictive power, they coexist beside one another, not atop one another.

Huh? To say "physics is just one more model" is not to say "the other useful models are on top of math and physics".

But they are, whether that's what you intended to say or not.

But they are, whether that's what you intended to say or not.

I suppose that will remain a point of disagreement.

You insist that all useful models are founded on physics, regardless of the historical and factual bases for those other models, regardless whether introducing a physics model does not offer additional predictive power to the models (and would thus be trimmed away by Occam's razor), and regardless of having little or no empirical validation for whichever specific physical reductions you hypothesize to exist (in the event you get past the hand-wavy '→' and work out some concrete details).

I once held similar beliefs, when I was first studying physics. But my study of secure distributed computing has affected my understanding of time, observation / interaction, and the nature of modeling.

I doubt you'll turn on this point, so I shall leave you to pursue your philosophy to its conclusions. May your pursuit of reductionism prove less fruitless than my own.

This sounds like the long running great debate on whether reductionism is even possible (much less useful, etc.).

While I take no firm position on this great debate, when I last traveled in philosophical circles, most folks seemed highly prejudiced against the reductionist agenda.

Re: comment-57439: What constitutes a powerful argument…? A long sentence with a lot of references to thoughts which are not your own?

A powerful argument is a chunk of text — hopefully one that argues for or against a point that may or not be germane to the topic under consideration — that you wouldn't be ashamed to include verbatim in your Ph.D. thesis.

  Aus einem Buch abschreiben ⇨ Plagiat;
  aus zwei Büchern abschreiben ⇨ Essay;
  aus drei ⇨ Kompilation;
  aus vier ⇨ Dissertation.
  Aus der Wikipedia ⇨ Hausarbeit.
         — Wilson Mizner

I don't really want to get sucked into this argument, but just a few remarks.

I think it is hard to compare these two things. For example, Maxwell and Navier-Stokes are "god-given" (or Maxwell-given or whatever).

Physics has to deal with two sets of laws: the laws of mathematics and the laws of the universe. Both are "God-given". Computer science has to deal only with the first, but these are God-given in your sense. Arguably, for practical matters, you also have to deal with the laws induced by the platform; but this is like in physics having to deal with the limitations of electronic or structural components produced by different vendors.

If you work in this field, you cannot do without them, because they describe certain facts in the best way known to mankind for describing basic physics, which is mathematics. Nobody needs Petri nets, message sequence charts, live sequence charts or statecharts to build software. This is just complicated notation for pretty simple things.

I'm not so sure about Petri nets, but for the rest I agree. I really don't understand why people make such a big deal out of them, and even formalize notation as with class diagrams, etc. If I want to talk about sequences or graphs, I do it mathematically, and I'd only draw charts for simple examples.

But I think your argument is misguided. An interior designer doesn't need Maxwell to design the lighting in a room, and a sailor doesn't need Navier-Stokes to steer a ship. Similarly, a programmer doesn't need to understand partial recursive functions to write software. The reason is that none of these people are technicians or engineers, and the tolerance for error or even failure is very high. Yes, I believe that programmers are not technicians/engineers. (In fact, they seem to want to be regarded as artists or craftsmen.)

Software engineers don't exist yet, but if they are going to exist at some point, they will need to be a class of professionals that exploit a mathematical foundation for software. Because that's what "engineering" is. The closest thing I have seen to software engineering is in "Deriving an X" papers like:

Richard S. Bird, Jeremy Gibbons, and Geraint Jones. Formal derivation of a pattern matching algorithm. Science of Computer Programming, 12(2):93-104, July 1989.

Peter Sestoft. Deriving a lazy abstract machine. In Journal of Functional Programming, vol 7, number 3, May 1997, pages 231-264.

Robert Harper. Proof-Directed Debugging. Journal of Functional Programming. 2000.

just think that computer science (the software branch) has not arrived at a comparable level (compared to physics) of sophistication yet. Maybe it never will.

I agree physics is far better developed than computer science. One of the reasons, though, might be that everyone in engineering agrees it should be based on physics, whereas programmers largely reject the idea that software should be based on computer science.

Because in physics we are bound by the laws of nature. With software, we are bound to a much lesser degree by the laws of nature, and to a much higher degree by our imagination. Therefore I think that too much formal education is dangerous.

You could say the same about pure mathematics, but would you argue that formal education in mathematics is dangerous for your mathematics career?

As an example, look at all that research that has been done into types. Yes, Hindley-Milner is useful. The rest of type theory that this has started, not so much :-)

I disagree, but I don't feel like arguing this point today.

I think that all arguments which are not proofs are pretty much a waste of time.

I pretty much agree.

With software, we are bound to a much lesser degree by the laws of nature, and to a much higher degree by our imagination.

"Modern programming languages have evolved through more than five decades of experience in constructing programmed solutions to complex, real-world problems. Modern programs can be quite complex, reaching sizes measured in millions of lines of code, written by large teams of human programmers over many years. In our view, languages that scale to this level of complexity are successful in part because they model some essential aspects of how to construct complex programs. In this sense, these languages are not just arbitrary constructions of the human mind. We would therefore like to understand them in a scientific way, i.e., by explaining their behavior in terms of a simple underlying model. This is the deep motivation behind the kernel language approach."

- CTM, page 36.

Re: comment-60206

Re: comment-57428:

With software, we are bound to a much lesser degree by the laws of nature, and to a much higher degree by our imagination.

Laws of software — they do exist

I read Steven's remark in the same spirit I read the one by Butler W. Lampson:

Although it's difficult to handle complexity in software, it's much easier to handle it there than elsewhere in a system. It's therefore good engineering to move as much complexity as possible into software.

It's not that there are no laws of software. It's just that software seems a lot more malleable than hardware.

I don't think it so relevant that we need to comprehend every model, so much as to recognize that the models themselves are incomplete and heuristic, and that we need effective ways to compose them as well as upgrade and maintain them at runtime.

In fact, attempting to comprehend and maintain every model you use is probably a mistake. For in-the-large programming, most of the models you'll ever use are probably written by someone with greater expertise than you, and will probably be maintained by someone with greater expertise than you, and may even be opaque or obfuscated to protect intellectual properties. Rather than comprehending every model, you often need only be able to query it, and to compose the result of said query into a new model or to decide intelligent behavior. Oh, and it's also useful to audit the model, to examine reputation, to determine the level of trust you're willing to place in it.

Some approaches:

Functional Reactive Programming (FRP): is a powerful yet efficient mechanism for model composition. Given separately maintained query, data, and model, one can easily construct an FRP expression that queries the model as applied to the data. The result of any FRP expression itself can be used in further such compositions. FRP inherently supports laziness, caching, data parallelism, and demand-driven properties. Judicious use of caching also allows some 'delta isolation'.

Complex Event Processing (CEP): is sort of the uber-generalization on model composition, including all of FRP but also allowing one to track histories and discrete events to make intelligent decisions. The outputs of a CEP model can include both reactive expressions and new discrete event sources.

CEP often pays for the generality in terms of efficiency. For example, demand-driven CEP is not always possible of the CEP model requires a history, and even slight use of internal state (even just incrementing a number, or tracking the last three or four messages received) tends to force centralized processing and thus hinders multi-cast performance, redundancy, resilience, reliability.

Using matchmakers, one might publish and combine 'pluggable' FRP and CEP models in some very interesting manners. I.e. new models could be added and removed dynamically, over time, so long as they match known interfaces. Of course, such an implementation probably should be careful to stratify the models, lest you end up with cyclic dependencies.

Rules-based Programming: given 'reactive' models, one can say 'when do '. Supposing the models themselves can be heavily composed from many perspectives, this becomes a powerful and general technique for in-the-large programming technique. OTOH, it can be difficult to predict and control: concurrency issues, feedback loops, etc.

Tuple Space or Blackboard Metaphor: multiple agents interact with a common database, each introducing his own perspective in a sort of round-table discussion. This approach is moderately popular, but I'm not very fond of it because it effectively glues all the models used by all the agents into one monolithic blob. That's a composition, sure, but it makes quite difficult any fine-grained reuse of just a subset of models, and it has questionable security properties.

...

Having good languages to create FRP expressions and CEP systems is, of course, useful and equivalent to having good modeling languages. But I think at that level you're back to 'programming-in-the-small'.

I honestly think people hear the phrase "programming in the large" and automatically assume they know what it means. Just like people hear the word "object" and automatically assume they know what it means. Just like people hear the catch phrase "Goto Statement Considered Harmful" automatically assume they know what it means. Just like people who hear "Premature optimization is the root of all evil" automatically assume they know what it means (and take it as an excuse for negligent design).

Headlines are no way to educate oneself.

For those who refuse to damage their brain with sensational headlines, and prefer instead to actually understand the meaning of things, please refer to the original 1975 paper Programming-in-the large versus programming-in-the-small.

We distinguish the activity of writing large programs from that of writing small ones. By large programs we mean systems consisting of many small programs (modules), possibly written bY different people.

We need languages for programming-in-the-small, i.e. languages not unlike the common programming languages of today, for writing modules. We also need a "module interconnection language" for knitting those modules together into an integrated whole and for providing an overview that formally records the intent of the programmer(s) and that can be checked for consistency by a compiler.

We explore the software r e l i a b i l i t y aspects of such an interconnection language. Emphasis is placed on facilities for information hiding and for defining layers of virtual machines.

Folks, this paper is 8 pages long and easy to read. Suffice to say, it is no mistake Roy Fielding's Ph.D. thesis makes much ado about module interconnection semantics. Avoiding programming-in-the-large doesn't make much sense. Sorry.

Ya, but it's behind a pay-gate.

On the link, Google provides 18 different versions. Click it and find a free one.

That's the whole reason I linked to Google Scholar.

nice paper, thanks. any thoughts on a current best chance at a good MIL?

I think asking what technology one should look at is simply a bad idea.

Most technology sucks.

Ever since undergrad I've been interested in separation logic and forcing programmer's to define exactly how to things should interact.

sure, presumably we start with a formalism of some kind, and then 'reify' that with some kind of automated checking, be it static type analysis or unit tests. (well, ok, maybe some people don't care about automated checking, but i think they are wrong to think that way.) point being that i think there will always be a technology involved. when i ask about e.g. which MIL does somebody like, i /ass/ume given the context (posting on LtU) people would talk about the goal (preferred formalism) and the means (current best technical implementation(s)).

i'll go read up on separation logic, thanks!

That paper has a nice statement of the problem... but a massively oversimplified solution.

It simply doesn't face up to the reality that Large Systems are built out of smaller systems "that grew up together".

So yes, you may make nice warm fuzzy block diagrams or even a MIL language to say how they join.....

But the devil is in the devilish details. When it comes down to whether almost any very large system works or not, it is the _exact_ calling signature AND THE SEQUENCE AND MANNER IN WHICH THEY'RE INVOKED that matters.

ie. The most devilishly detailed MIL such as Corba is not detailed enough, as it doesn't specify the intimate details that came into being as the two smaller systems grew up together.

The real reason for the success of the unixy ecosystem is ignorance. Ignorance of who or what is on the other side.

As soon as you declare a program is part of a system, short cuts are taken. Far better is to declare each smaller program to be utterly stand-alone, taking input and sending output to as yet unspecified other programs.

Even REST is the latest in a long line of examples of how software fits into the definition of a service, not a "set of instructions"! Maybe a program fits into the latter definition, but the problem with that is that people use the words "software" and "program" interchangeably!

I propose we change the definition of "software"!

Given that the Unix pipes use generally text based format (which is quite fragile), I wouldn't call this 'very contrained' interfaces.

I meant, compared to being able to call arbitrary functions in another module, UNIX's classic unidirectional pipes are constrained.

This drastic extrusion of semantics constituted true rigor; mathematics itself would be suspect as long as there was any vestige of meaning or semantics left in it.

Yeah, mathematicians hate this. It reminds me of a quote from Dijkstra:

And from the mathematical community I have learned not to expect too much support either, as informality is the hallmark of the Mathematical Guild, whose members —like poor programmers— derive their intellectual excitement from not quite knowing what they are doing and prefer to be thrilled by the marvel of the human mind (in particular their own ones). For them, the Dream of Leibniz is a Nightmare.

I for one am a believer. Sure, we know that not everything can be automated, but people seem to very seriously under-estimate how much can be. For example, the vast majority of useful functions tend to have termination proofs; sure, not all of them do, but the exceptions are rather rare (or contrived, aka not useful). Naturally that's just my opinion, but I am putting my own time behind those beliefs. For example, the PL that I am currently working on has a type system for which type-checking is (wildly) undecidable; yet all the code we've written until now has type-checked nicely and efficiently.

As an additional post scriptum I can't help but wonder how much of the debate--and others like it--is more about disputes over the scope and definition of the field known as "Computer Science" than it is about actual substantive disagreements.

The issue of programming-in-the-large seems to magnify these sorts of disputes, as it touches on issues of computation theory, engineering, and social dynamics of organization, all in a deeply interwoven way.

Hand-waving philosophy is as useless for describing computation as rigid mathematical formalisms are for managing social dynamics, which is why I complain about broad definitions: trying to apply a single theoretical framework to all of it is practically guaranteed to produce rubbish and nonsense at best.

I'm sure this has been discussed on LtU before, though a quick search found me only other tangentially related discussions.

You've succinctly said what I spent many more posts and many hundreds, if not thousands, of words attempting, ineptly, to say.

it is more about disputes over the scope and definition of the field known as "Computer Science" than it is about actual substantive disagreements

Well it is often a bit like placing physics and mathematics into a single science and then being offended when physics minded people don't care about 99% of what mathematicians do. They extract value for computing their stuff but never proof anything and they don't see much merit in doing so. No one gives up quantum field theory just because it is mathematically inconsistent.

Well it is often a bit like placing physics and mathematics into a single science and then being offended when physics minded people don't care about 99% of what mathematicians do.

To my eye, the state of affairs with CS is something more akin to founding a field of "House-Building Science" with a mixture of solid-state physicists, bricklayers, and interior decorators, then wondering why 1) Nobody talks to anybody else and 2) The typical end results are expensive, ugly, and prone to falling down.

Re: comment-60282:

The typical end results are expensive, ugly, and prone to falling down.

You almost make it sound like the field is in some sort of crisis, n'est-ce pas? Is there really a crisis? Butler Lampson thinks that there isn't.

You almost make it sound like the field is in some sort of crisis

Au contraire, the frequent failure of large software projects and the poor quality of many that succeed may be regrettable, but clearly do not constitute a crisis, on the empirical grounds that, statistically speaking, nobody cares.

There is much that could be said about group behavior and competitive pressure in general, but the end result is that quality and efficiency are valued only up to the minimum required. Examples of absurd incompetence found in software development are, in actual fact, mostly demonstrations of what happens when people undertake tasks in an environment where failure is cheap and success unrewarded, as is the case in most large organizations.

Re: comment-60290 (emphasis mine):

Examples of absurd incompetence found in software development are, in actual fact, mostly demonstrations of what happens when people undertake tasks in an environment where failure is cheap and success unrewarded, as is the case in most large organizations.

Your penetrating insights expressed in your fluid and effortless English prompted me to check some of your previous posts in hope of digging up a few more pithy and aphoristic observations. I found the analysis of COME FROM incisive.

But I digress…

Listening to people bitch and groan about the allegedly sorry state of software development, one may be forgiven for getting the impression that the rest of the world delivers their sh^Htuff on time and under budget; that the following projects are exceptional in their lateness and cost overruns:

• Red Line of the Dubai Metro
• Ski Dubai

A little closer to home:

• Big Dig
• The Hancock Tower
• Stata Center

To lift a quote from the latter:

On October 31, 2007, MIT sued architect Frank Gehry and the construction company, Skanska USA Building Inc., for “providing deficient design services and drawings” which caused leaks to spring, masonry to crack, mold to grow, drainage to back up, and falling ice and debris to block emergency exits.

I guess Gehry neglected to base his design on whatever it is that construction engineers consider to be the foundational equivalent of SK combinators.

For probably the first time, I actually think you give me too little credit. :-)

Search the site, and you'll find some posts from me on "Proof Polynomials" and the Logic of Provability, Sergei Artemov's program to fulfill Gödel's desire to see a formal semantics of the BHK interpretation of logic.

I've also written many times about the influence of Jaynes' "Probability Theory: The Logic of Science" on my thinking, in particular that we use Cox's theorem when we don't have all the information, and (the rest of) logic when we do. Couple this with the work on Algorithmic Information Theory, and you have a very fruitful toolbox for reasoning, including statistical inference. I should also add Peter Grünwald's "The Minimum Description Length Principle" to the list. Jaynes in particular, though, has very strong things to say about Gödel's result: that, once the role of information in logic/probability is properly understood, Gödel's result is properly seen as obvious, a tautology, rather than as a source of horror or even limitation: it just means that the axiom system under consideration doesn't contain enough information to prove its own consistency. So what?

So I don't think of this work from the Santa Fe Institute as hand-waving at all. But it does read like it's behind the current state-of-the-art in thinking about the issues.