1. 18

I believe that the “single entry, single exit” coding style has not been helpful for a very long time, because other factors in how we design programs have changed.

Unless it happens that you still draw flowcharts, anyway. The first exhortation for “single entry, single exit” I can find is Dijkstra’s notes on structured programming, where he makes it clear that the reason for requiring that is so that the flowchart description of a subroutine has a single entry point and a single exit point, so its effect on the whole program state can be understood by understanding that subroutine’s single collection of preconditions and postconditions. Page 19 of the PDF linked above:

These flowcharts share the property that they have a single entry at the top and a single exit at the bottom: as indicated by the dotted block they can again be interpreted (by disregarding what is inside the dotted lines) as a single action in a sequential computation. To be a little bit more precise” we are dealing with a great number of possible computations, primarily decomposed into the same time-succession of subactions and it is only on closer inspection–i.e, by looking inside the dotted block–that it is revealed that over the collection of possible computations such a subaction may take one of an enumerated set of distinguished forms.

These days we do not try to understand the behaviour of a whole program by composing the behaviour of each expression. We break our program down into independent modules, objects and functions so that we only need to understand the “inside” of the one we’re working on and the “outside” of the rest of them (the “dotted lines” from Dijkstra’s discussion), and we have type systems, tests and contracts to support understanding and automated verification of the preconditions and postconditions of the parts of our code.

In other words, we’re getting the benefits Dijkstra wanted through other routes, and not getting them from having a single entry point and a single exit point.

1. 7

An interesting variant history is described in https://softwareengineering.stackexchange.com/a/118793/4025

The description there is that instead of “single exit” talking about where the function exits from, it actually talks about a function only having a single point it returns to, namely the place where it was called from. This makes a lot more sense, and is clearly a good practice. I’ve heard this description from other places to, but unfortunately I don’t have any better references.

1. 3

Yes, very interesting. It makes sense that “single exit” means “don’t jump to surprising places when you’re done” rather than “don’t leave the subroutine from arbitrary places in its flow”. From the Structured Programming perspective, both support the main goal: you can treat the subroutine as a box that behaves in a single, well-defined way, and that programs behave as a sequence of boxes that behave in single, well-defined ways.

2. 3

The first exhortation for “single entry, single exit” I can find is Dijkstra’s notes on structured programming

Also Tom Duff’s “Reading Code From Top to Bottom” says this:

During the Structured Programming Era, programmers were often taught a style very much like the old version. The language they were trained in was normally Pascal, which only allowed a single return from a procedure, more or less mandating that the return value appear in a variable. Furthermore, teachers, influenced by Bohm and Jacopini (Flow Diagrams, Turing Machines and Languages with only two formation rules, Comm. ACM 9#5, 1966, pp 366-371), often advocated reifying control structure into Boolean variables as a way of assuring that programs had reducible flowgraphs.

1. 1

These days we do not try to understand the behaviour of a whole program by composing the behaviour of each expression. We break our program down into independent modules, objects and functions so that we only need to understand the “inside” of the one we’re working on and the “outside” of the rest of them (the “dotted lines” from Dijkstra’s discussion), and we have type systems, tests and contracts to support understanding and automated verification of the preconditions and postconditions of the parts of our code.

Maybe I’m missing something, but it seems to me that Dijkstra’s methodology supports analyzing one program component at a time, treating all others as black boxes, so long as:

• Program components are hierarchically organized, with lower-level components never calling into higher-level ones.
• Relevant properties of lower-level components (not necessarily the whole analysis) are available when analyzing higher-level components.

In particular, although Dijkstra’s predicate transformer semantics only supports sequencing, selection and repetition, it can be used to analyze programs with non-recursive subroutines. However, it cannot handle first-class subroutines, because such subroutines are always potentially recursive.

In other words, we’re getting the benefits Dijkstra wanted through other routes, and not getting them from having a single entry point and a single exit point.

Dijkstra’s ultimate goal was to prove things about programs, which few of us do. So it is not clear to me that we are “getting the benefits he wanted”. That being said, having a single entry point and a single exit point merely happens to be a requirement for using the mathematical tools he preferred. In particular, there is nothing intrinsically wrong about loops with two or more exit points, but they are awkward to express using ALGOL-style while loops.

1. 3

We can do ADTs with objects trivially, too. With our running Coord example, some languages allow “sealed interfaces” where the only implementations can be those in the same package. But otherwise just say “don’t implement this yourself, you’ve been warned.” Good enough.

No, it’s not good enough. Try providing two implementations of the following abstract data type specification using objects:

(* Purely functional, guaranteed non-empty heaps.
* No exceptions are thrown under any circumstances. *)
signature HEAP =
sig
type key
type heap
val pure : key -> heap (* singleton constructor *)
val head : heap -> key
val tail : heap -> heap option
val ++ : heap * heap -> heap
end


You can’t.

I call sealed (i.e. “no subclassing”) classes “abstract data types.”

Again, no. The whole point to abstract data types is that users don’t need to know or care how they are implemented.

I think ADTs are best represented as classes not intended for subclassing.

Abstract data types are best internally represented as ordinary data structures. Even the intermediate states of manipulating complex data structures are best represented as ordinary data structures.

With objects and ADTs, you can think in terms of properties: preconditions, postconditions, invariants, and the like for simple cases.

This is true for abstract data types, but not objects. Type abstraction is precisely the mechanism that guarantees that an established invariant cannot be destroyed by third parties.

With a functional language, we can:

• For ADTs, just don’t export a data type’s constructors from its module.

That’s what Haskell does, and it’s pretty terrible. Other languages provide more graceful type abstraction facilities.

1. 1

I fail to see the point. Writing arbitrary code and only then figuring out what equational laws it satisfies is… errr… technically possible, but methodologically backwards.

1. 5

I do it, especially when working with other code other teams or people have written:

https://developer.atlassian.com/blog/2016/03/programming-with-algebra/

1. 1

That was a very cool example, thanks.

1. 3

You can pretend you can do functional programming in any language, but what use is it if you don’t get any support from the language’s semantics? If “functional programming” is intended to be more than just another buzzword, its technical meaning[0] has to be something along these lines:

Functional programming is a programming style in which the problem domain is modeled as a collection of values, and the problem’s solution is implemented as a collection of procedures that evaluate functions, i.e., mappings from values to values.

Hence, the bare minimum one can demand in a language for “doing functional programming” is:

• The ability to define problem-domain values, abstracting away the details of their physical representation, such as the number of independently allocated memory blocks used to store this representation in memory.
• A purely syntactic criterion for establishing that a procedure evaluates a function, and a large class of functions that can be efficiently evaluated by procedures that satisfy this criterion.

If your language gives you less than this, then either “doing functional programming” is bound to be an uphill struggle (in which case you should consider switching to a style that makes life less difficult) or you will have to relax the definition of what “functional programming” means (in which case you need to argue that your revised definition is still meaningful).

[0] Note that I’m not saying functional programming is unquestionably a good thing. My purpose is just to give a technically precise criterion for when one is “doing functional programming”.

1. 1

The article makes a really important observation that’s often overlooked. It’s really important for code to express its intent clearly. The key to working with code effectively lies in your ability to understand its purpose. Static typing can have a big impact on the way we structure code, and in many cases it can actually obscure the bigger picture as the article illustrates.

1. 20

I don’t see how the article illustrates that. The article’s argument is that converting between serialization format and your business object requires maintaining some other kind of code and that costs something.

In my experience I’ve had other costs, which I found more expensive, in dealing with using one’s serialization layer as a business object:

1. The expected fields and what they are tend to not be well documented. Just convert the JSON and use it as a dict or whatever, but it’s hard to know what should be there for someone who didn’t write the code. With static types, even if one doesn’t document the values, they are there for me to see.
2. The semantics of my serialization layer may not match the semantics of my language and, more importantly, what I want to express in my business logic. For example, JSON’s lack of integers.
3. The serialization changes over versions of the software but there is a conversion to the business object that still makes sense, I can do that at the border and not affect the rest of my code.

The call out to clojure.spec I found was a bit odd as well, isn’t that just what any reasonable serialization framework is doing for you?

As a static type enthusiast, I do not feel that the conversion on the edges of my program distract from some bigger picture. I do feel that after the boundary of my program, I do not want to care what the user gave me, I just want to know that it is correct. If one’s language supports working directly with some converted JSON, fine.

On another note, I don’t understand the Hickey quote in this article. What is true of all cars that have driven off a road with a rumble strip? They went over the rumble strip. But cars drive off of roads without rumble strips too, so what’s the strength of that observation? Does the lack of a rumble strip some how make you a more alert driver? Do rumble strips have zero affect on accidents? I don’t know, but in terms of static types, nobody knows because the studies are really hard to do. This sort of rhetoric is just distracting and worthless. In my experience, the talk of static types and bugs is really not the strength. I find refactoring and maintenance to be the strength of types. I can enter a piece of code I do not recognize, which is poorly documented, and start asking questions about the type of something and get trustworthy answers. I also find that that looking at the type of a function tends to tell me a lot about it. Not always, but often enough for me to find it valuable. That isn’t to say one shouldn’t document code but I find dynamically typed code tends to be as poorly documented as any other code so I value the types.

If one doesn’t share that experience and/or values, then you’ll disagree, and that’s fine. I’m not saying static types are objectively superior, just that I tend to find them superior. I have not found a program that I wanted to express that I preferred to express with a dynamic language. I say this as someone that spends a fair amount of time in both paradigms. The lack of studies showing strengths in one direction or another doesn’t mean dynamic types are superior to static or vice versa, it just means that one can’t say one way or the other and most of these blog posts are just echos of one’s experience and values. I believe this blog post is falling into the trap of trying to find some explanatory value in the author’s experience when in reality, it’s just the author’s experience. I wish these blog posts started with a big “In my experience, the following has been true….”

Disclaimer, while I think Java has some strengths in terms of typing, I really much prefer spending my time in Ocaml, which has a type system I much prefer and that is generally what I mean when I say “static types”. But I think in this comment, something like Java mostly applies a well.

1. 3

The call out to clojure.spec I found was a bit odd as well, isn’t that just what any reasonable serialization framework is doing for you?

My experience is that Clojure spec addresses the three points. However, Spec can live on the side as opposed to being mixed with the implementation, and it allows you to only specify/translate the types for the specific fields that you care about. I think this talk does a good job outlining the differences between the approaches.

On another note, I don’t understand the Hickey quote in this article.

What you ultimately care about is semantic correctness, but type systems can actually have a negative impact here. For example, here’s insertion sort implemented in Idris, it’s 260 lines of code. Personally, I have a much time understanding that the following Python version is correct:

def insertionsort( aList ):
for i in range( 1, len( aList ) ):
tmp = aList[i]
k = i
while k > 0 and tmp < aList[k - 1]:
aList[k] = aList[k - 1]
k -= 1
aList[k] = tmp


I can enter a piece of code I do not recognize, which is poorly documented, and start asking questions about the type of something and get trustworthy answers.

I’ve worked with static languages for about a decade. I never found that the type system was a really big help in this regard. What I want to know first and foremost when looking at code I don’t recognize is the intent of the code. Anything that detracts from being able to tell that is a net negative. The above example contrasting Idris and Python is a perfect example of what I’m talking about.

Likewise, I don’t think that either approach is superior to the other. Both appear to work effectively in practice, and seem to appeal to different mindsets. I think that alone makes both type disciplines valuable.

It’s also entirely possible that the language doesn’t actually play a major role in software quality. Perhaps, process, developer skill, testing practices, and so on are the dominant factors. So, the right language inevitably becomes the one that the team enjoys working with.

1. 7

That’s not a simple sort in Idris, it’s a formal, machine checked proof that the implemented function always sorts. Formal verification is a separate field from static typing and we shouldn’t conflate them.

For the record, the python code fails if you pass it a list of incomparables, while the Idris code will catch that at compile time.

I’m a fan of both dynamic typing and formal methods, but I don’t want to use misconceptions of the latter used to argue for the former.

1. 1

machine checked proof that the implemented function always sorts.

And if comparing spec vs test sizes apples to apples, that means we need a test for every possible combination of every value that function can take to be sure it will work for all of them. On 64-bit systems, that’s maybe 18,446,744,073,709,551,615 values per variable with a multiplying effect happening when they’re combined with potential program orderings or multiple variable inputs. It could take a fair amount of space to code all that in as tests with execution probably requiring quantum computers, quark-based FPGA’s, or something along those lines if tests must finish running in reasonable time. There’s not a supercomputer on Earth that could achieve with testing what assurance some verified compilers or runtimes got with formal verification of formal, static specifications.

Apples to apples, the formal specs with either runtime checks or verification are a lot smaller, faster, and cheaper for total correctness than tests.

2. 3

For example, here’s insertion sort implemented in Idris, it’s 260 lines of code. (…) Personally, I have a much time understanding that the following Python version is correct: (snippet)

An actually honest comparison would include a formal proof of correctness of the Python snippet. Merely annotating your Python snippet with pre- and postcondition annotations (which, in the general case, is still a long way from actually producing a proof) would double its size. And this is ignoring the fact that many parts in your snippet have (partially) user-definable semantics, like the indexing operator and the len function. Properly accounting for these things can only make a proof of correctness longer.

That being said, that a proof of correctness of insertion sort takes 260 lines of code doesn’t speak very well of the language the proof is written in.

What I want to know first and foremost when looking at code I don’t recognize is the intent of the code.

Wait, the “intent”, rather than what the code actually does?

1. 1

An actually honest comparison would include a formal proof of correctness of the Python snippet.

That’s not a business requirement. The requirement is having a function that does what was intended. The bigger point you appear to have missed is that a complex formal specification is itself a program! What method do you use to verify that the specification is describing the intent accurately?

Wait, the “intent”, rather than what the code actually does?

Correct, these are two entirely different things. Verifying that the code does what was intended is often the difficult task when writing software. I don’t find static typing to provide a lot of assistance in that regard. In fact, I’d say that the Idris insertion sort implementation is actually working against this goal.

1. 4

The bigger point you appear to have missed is that a complex formal specification is itself a program!

This is not true. The specification is a precondition-postcondition pair. The specification might not even be satisfiable!

What method do you use to verify that the specification is describing the intent accurately?

Asking questions. Normally users have trouble thinking abstractly, so when I identify a potential gap in a specification, I formulate a concrete test case where what the specification might not match the user’s intention, and I ask them what the program’s intended behavior in this test case is.

I don’t find static typing to provide a lot of assistance in that regard.

I agree, but with reservations. Types don’t write that many of my proofs for me, but, under certain reasonable assumptions, proving things rigorously about typed programs is easier than proving the same things equally rigorously about untyped programs.

1. 1

This is not true. The specification is a precondition-postcondition pair. The specification might not even be satisfiable!

A static type specification is a program plain and simple. In fact, lots of advanced type systems. such as one found in Scala, are actually Turing complete. The more things you try to encode formally the more complex this program becomes.

Asking questions. Normally users have trouble thinking abstractly, so when I identify a potential gap in a specification, I formulate a concrete test case where what the specification might not match the user’s intention, and I ask them what the program’s intended behavior in this test case is.

So, how is this different from what people do when they’re writing specification tests?

1. 2

A static type specification is a program plain and simple.

Not any more than a (JavaScript-free) HTML document is a program for your browser to run.

In fact, lots of advanced type systems. such as one found in Scala, are actually Turing complete.

I stick to Standard ML, whose type system is deliberately limited. Anything that can’t be verified by type-checking (that is, a lot), I prove by myself. Both the code and the proof of correctness end up simpler this way.

So, how is this different from what people do when they’re writing specification tests?

I am not testing any code. I am testing whether my specification captures what the user wants. Then, as a completely separate step, I write a program that provably meets the specification.

1. 1

I stick to Standard ML, whose type system is deliberately limited. Anything that can’t be verified by type-checking (that is, a lot), I prove by myself. Both the code and the proof of correctness end up simpler this way.

At that point it’s really just degrees of comfort in how much stuff you want to prove statically at compile time. I find that runtime contracts like Clojure Spec are a perfectly fine alternative.

I am testing whether my specification captures what the user wants.

I’ve never seen that done effectively using static types myself, but perhaps you’re dealing with a very different domain from the ones I’ve worked in.

1. 1

At that point it’s really just degrees of comfort in how much stuff you want to prove statically at compile time.

This is not a matter of “degree” or “comfort” or “taste”. Everything has to be proven statically, in the sense of “before the program runs”. However, not everything has to be proven or validated by a type checker. Sometimes directly using your brain is simpler and more effective.

I am testing whether my specification captures what the user wants.

I’ve never seen that done effectively using static types myself

Me neither. I just use the ability to see possibilities outside the “happy path”.

1. 1

However, not everything has to be proven or validated by a type checker.

I see that as a degree of comfort. You’re picking and choosing what aspects of the program you’re going to prove formally. The range is from having a total proof to having no proof at all.

Sometimes directly using your brain is simpler and more effective.

Right, and the part we disagree on is how much assistance we want from the language and in what form.

1. 1

You’re picking and choosing what aspects of the program you’re going to prove formally.

I’m not “picking” anything. I always prove rigorously that my programs meet their functional specifications. However, my proofs are meant for human rather than mechanical consumption, hence:

• Proofs cannot be too long.
• Proofs cannot demand simultaneous attention to more detail than I can handle.
• Abstractions are evaluated according to the extent to which they shorten proofs and compartmentalize details.

Right, and the part we disagree on is how much assistance we want from the language and in what form.

The best kind of “assistance” a general-purpose language can provide is having a clean semantics and getting out of the way when it can’t help. If you ever actually try to prove a program[0] correct, you will notice that:

• Proving that a control flow point is unreachable may require looking arbitrarily far back into the history of the computation. Hence, you want as few unreachable control flow points as possible, preferably none.

• Proving that a procedure call computes a result of interest requires making assumptions about the procedure’s precondition-postcondition pair. For second-class (statically dispatched) procedure calls, these assumptions can be discharged immediately—you know what procedure will be called. For first-class (dynamically dispatched) procedure calls, these assumptions may only be discharged in a very remote[1] part of your program. Hence, first-class procedures ought to be used sparingly.

[0] Actual programs, not just high-level algorithm descriptions that your programs allegedly implement.

[1] One way to alleviate the burden of communicating precondition-postcondition requirements between far away parts in a program is to systematically use so-called type class laws, but this is not a widely adopted solution.

1. 1

Right, and the other approach to this problem is to use runtime contracts such as Clojure Spec. My experience is that this approach makes it much easier to express meaningful specifications. I’m also able to use it where it makes the most sense, which tends to be at the API level. I find there are benefits and trade-offs in both approaches in practice.

1. 1

Right, and the other approach to this problem is to use runtime contracts such as Clojure Spec.

This is not a proof of correctness, so no.

I’ve already identified two things that don’t help: runtime checks and overusing first-class procedures. Runtime-checked contracts have the dubious honor of using the latter to implement the former in order to achieve nothing at all besides making my program marginally slower.

My experience is that this approach makes it much easier to express meaningful specifications.

I can already express meaningful specifications in many-sorted first-order logic. The entirety of mathematics is available to me—why would I want to confine myself to what can be said in a programming language?

I’m also able to use it where it makes the most sense, which tends to be at the API level.

It makes the most sense before you even begin to write your program.

1. 2

This is not a proof of correctness, so no.

I think this is the key disconnect we have here. My goal is to produce working software for people to use, and writing a proof of correctness is a tool for achieving that. There are other viable tools that each have their pros and cons. My experience tells me that writing proofs of correctness is not the most effective way to achieve the goal of delivering working software on time. Your experience clearly differs from mine, and that’s perfectly fine.

I can already express meaningful specifications in many-sorted first-order logic. The entirety of mathematics is available to me—why would I want to confine myself to what can be said in a programming language?

You clearly would not. However, there are plenty of reasons why other people prefer this. A few reasons of top of my head are the following. It’s much easier for most developers to read runtime contracts. This means that it’s easier to onboard people and train them. The contracts tend to be much simpler and more expressive. This makes it easier to read and understand them. They allow you to trivially express things that are hard to express at compile time. Contracts can be used selectively in places where they make the most sense. Contracts can be open while types are closed.

It makes the most sense before you even begin to write your program.

Again, we have a very divergent experience here. I find that in most situations I don’t know the shape of the data up front, and I don’t know what the solution is going to be ultimately. So, I interactively solve problems using a REPL integrated editor. I might start with a particular approach, scrap it, try something else, and so on. Once I settle on a way I want to do things, I’ll add a spec for the API.

Just to be clear, I’m not arguing that my approach is somehow better, or trying to convince you to use it. I’m simply explaining that having tried both, I find it works much better for me. At the same time, I’ve seen exactly zero empirical evidence to suggest that your approach is more effective in practice. Given that, I don’t think we’re going to gain anything more from this conversation. We’re both strongly convinced by our experience to use different tools and workflows. It’s highly unlikely that we’ll be changing each others minds here.

Cheers

1. 2

The contracts tend to be much simpler and more expressive. (…) Contracts can be open while types are closed.

I said “first-order logic”, not “types”. Logic allows you to express things that are impossible in a programming language, like “what is the distribution of outputs of this program when fed a sample of a stochastic process?”—which your glorified test case generator cannot generate.

Just to be clear, I’m not arguing that my approach is somehow better, or trying to convince you to use it. I’m simply explaining that having tried both, I find it works much better for me.

I’m not trying to convince you of anything either, but I honestly don’t think you have tried using mathematical logic. You might have tried, say, Haskell or Scala, and decided it’s not your thing, and that’s totally fine. But don’t conflate logic (which is external to any programming language) with type systems (which are often the central component of a programming language’s design, and certainly the most difficult one to change). It is either ignorant or dishonest.

2. 1

You can do more with a formal spec than a test. They can be used to generate equivalent tests for one like in EiffelStudio. Then, they can be used with formal methods tools, automated or full style, to prove they hold for all values. They can also be used to aid optimization by the compiler like in examples ranging from Common LISP to Strongtalk I gave you in other comment. There’s even been some work on natural language systems for formal specs which might be used to generate English descriptions one day.

So, one gets more ROI out of specs than tests alone.

1. 2

That’s why I find Clojure Spec to be a very useful tool. My experience is that runtime contracts are a better tool for creating specifications. Contracts focus on the usage semantics, while I find that types only have an indirect relationship with them.

At the same time, contracts are opt in, and can be created where they make the most sense. I find this happens to be at the boundaries between components. I typically want to focus on making sure that the API works as intended.

1. 2

Forgot to say thanks for Clojure spec link. That was a nice write-up. Good they added that to Clojure.

2. 1

“A static type specification is a program plain and simple. “

I dont think so but I could be wrong. My reading in formal specs showed they were usyally precise descriptions of what is to be done. The program is almost always a description of how to do something in a series of steps. Those are different things. Most formal specs arent executable on their own either since they’re too abstract.

There are formal specifications of how something is done in a concrete way that captures all its behaviors like with seL4. You could call those programs. The other stuff sounds different, though, since it’s about the what or too abstract to produce the result the programmer wants. So, I default on not a program with some exceptions.

1. 2

It’s a metaprogam that’s executed by the compiler with your program as the input. Obviously, you can have very trivial specifications that don’t really qualify as programs. However, you also have very complex specifications as well. There’s even a paper on implementing a type debugger for Scala. It’s hard to argue that specifications that need a debugger aren’t programs.

1. 1

I think this boils down to the definition of “program.” We may have different ones. Mine is an executable description of one or more steps that turn concrete inputs into concrete outputs optionally with state. A metaprogram can do that: it does it on program text/symbols. A formal specification usually can’t do that due to it being too abstract, non-executable, or having no concept of I/O. They are typically input too some program or embedded in one. I previously said some could especially in tooling like Isabelle or Prolog.

So, what is your definition of a program so I can test whether formal specs are programs or metaprograms against that definition? Also, out of curiosity too.

1. 2

My definition is that a program is a computational process that accepts some input, and produces some output. In case of the type system, it accepts the source code as its input, and decides whether it matches the specified constraints.

1. 1

Well, I could see that. It’s an abstract equivalent to mine it looks like. I’ll hold of debating that until I’m more certain of what definition I want to go with.

3. 3

That’s not a business requirement. The requirement is having a function that does what was intended

You’re comparing two separate things, though! The Idris isa proven correct function, while the python is just a regular function. If all the business wants is a “probably correct” function, the Idris code would be just a few lines, too.

1. 1

The point here is that formalism does not appear to help ensure the code is doing what’s intended. You have to be confident that you’re proving the right thing. The more complex your proof is, the harder it becomes to definitively say that it is correct. Using less formalism in Python or Idris results in code where it’s easier for the human reader to tell the intent.

1. 4

You can say your proof is correct because you have a machine check it for you. Empirically, we see that formally verified systems are less buggy than unverified systems.

1. 2

Machine can’t check that you’re proving what was intended. A human has to understand the proof and determine that it matches their intent.

1. 2

A human had to check the intent (validate) either way. A machine can check the implementation is correct (verify).

Like in the Idris, I have to validate that the function is supposed to sort. Once I know that’s the intention, I can be assured that it does, in fact, sort, because I have a proof.

1. 1

What I’m saying is that you have to understand the proof, and that can be hard to do with complex proofs. Meanwhile, other methods such as runtime contracts or even tests, are often easier to understand.

1. 1

That’s not how formal verification works, though. Let’s say my intention is “sort a list.” I write a function that I think does this. Then I write a formal specification, like “\A j, k \in 1..Len(sorted): j < k => sorted[j] <= sorted[k]”. Finally, I write the proof.

I need to validate that said specification is what I want. But the machine can verify the function matches the specification, because it can examine the proof.

1. 1

The fact that we’re talking past each other is a good illustration of the problem I’m trying to convey here. I’m talking about the human reader having to understand specifications like \A j, k \in 1..Len(sorted): j < k => sorted[j] <= sorted[k], only much longer. It’s easy to misread a symbol, and misinterpret what is being specified.

1. 2

You did say “have to understand the proof” (not specification) before. I strongly agree with the latter - the language we use for writing specs can easily get so complex that the specs are more error-prone than their subjects.

I once wrote a SymEx tool for PLCs and found that specs in my initial choice of property language (LTL) were much harder to get right than the PLC code itself. I then looked at the properties that would likely need to be expressed, and cut the spec language down to a few higher-level primitives. This actually helped a lot.

Even if restricting the property language isn’t an option, having a standard library (or package ecosystem) of properties would probably get us rather close - so instead of \A j, k \in ... we could write Sorted(s) and trust the stdlib / package definition of Sorted to do its name justice.

2. 4

For example, here’s insertion sort implemented in Idris, it’s 260 lines of code

When this code sample has been brought up before (perhaps by you) it’s been pointed out that this is not expected to be a production implementation and more of an example of playing with the type system. There is plenty of Python golf code out there too that one could use as an example to make a point. But, if we are going to compare things, the actual implementation of sort in Python is what..several hundred lines of C code? So your Python insertion sort might be short and sweet, but no more the production code people use than the Idris one. But if the Idris one were the production implementation, I would rather spend time understanding it than the Python sort function.

It’s also entirely possible that the language doesn’t actually play a major role in software quality. Perhaps, process, developer skill, testing practices, and so on are the dominant factors.

That is likely true, IMO. I think it’s interesting that one could replace type system in the Hickey quote with “testing” or “code review” and the statement would still be true, but people seem to zero in on types. No-one serious says that we shouldn’t have testing because we still have bugs in software.

I never found that the type system was a really big help in this regard. What I want to know first and foremost when looking at code I don’t recognize is the intent of the code.

My experience has definitely not been this. Right now I’m doing maintenance on some code and it has a call in it: state.monitors.contains(monitor) and I don’t have a good way to figuring out what state or monitors is without grepping around in the code. In Ocaml I’d just hit C-t and it’d tell me what it is. I find this to be a common pattern in my life as I have tended to be part of the clean-up crew in projects lately. The intent of that code is pretty obvious, but that doesn’t help me much for the refactoring I’m doing. But experiences vary.

1. 2

When this code sample has been brought up before (perhaps by you) it’s been pointed out that this is not expected to be a production implementation and more of an example of playing with the type system.

The point still stands though, the more properties you try to encode formally the more baroque the code gets. Sounds like you’re agreeing that it’s often preferable to avoid such formalisms in production code.

But, if we are going to compare things, the actual implementation of sort in Python is what..several hundred lines of C code? So your Python insertion sort might be short and sweet, but no more the production code people use than the Idris one.

The sort implementation in Python handles many different kinds of sorts. If you took the approach of describing all of the hundreds of lines of C of that with types in Idris, that would result in many thousands lines of code. So, you still have the same problem there.

No-one serious says that we shouldn’t have testing because we still have bugs in software.

People argue regarding what kind of testing is necessary or useful all the time though. Ultimately, the goal is to have a semantic specification, and to be able to tell that your code conforms to it. Testing is one of the few known effective methods for doing that. This is why some form of testing is needed whether you use static typing or not. To put it another way, testing simply isn’t optional for serious projects. Meanwhile, many large projects are successfully developed in dynamic languages just fine.

My experience has definitely not been this. Right now I’m doing maintenance on some code and it has a call in it: state.monitors.contains(monitor) and I don’t have a good way to figuring out what state or monitors is without grepping around in the code.

In Clojure, I’d just hit cmd+enter from the editor to run the code in the REPL and see what a monitor looks like. My team has been working with Clojure for over 8 years now, and I often end up working with code I’m not familiar with.

1. 3

Sounds like you’re agreeing that it’s often preferable to avoid such formalisms in production code.

At the moment, yes. I am not a type theorist but as far as I have seen, dependent types are not at the point where we know how to use them in effectively in a production setting yet. But I do make pretty heavy use of types elsewhere in codebases I work on when possible and try to encode what invariants I can in them when possible (which is pretty often).

If you took the approach of describing all of the hundreds of lines of C of that with types in Idris, that would result in many thousands lines of code. So, you still have the same problem there.

Maybe! I don’t actually know. The types in the Idris implementation might be sufficient to get very performant code out of it (although I doubt it at this point).

In Clojure, I’d just hit cmd+enter from the editor to run the code in the REPL …

I don’t know anything about Clojure, in the case I’m working on, running the code is challenging as the part I’m refactoring needs a bunch of dependencies and data and constructs different things based on runtime parameters. Even if I could run it on my machine I don’t know how much I’d trust it. The power of dynamic types at work.

1. 2

I don’t know anything about Clojure, in the case I’m working on, running the code is challenging as the part I’m refactoring needs a bunch of dependencies and data and constructs different things based on runtime parameters. Even if I could run it on my machine I don’t know how much I’d trust it. The power of dynamic types at work.

There is a fundamental difference in workflows here. With Clojure, I always work against a live running system. The REPL runs within the actual application runtime, and it’s not restricted to my local machine. I can connect a REPL to an application in production, and inspect anything I want there. In fact, I have done just that on many occasions.

This is indeed the power of dynamic types at work. Everything is live, inspectable, and reloadable. The reality is that your application will need to interact with the outside world you have no control over. You simply can’t predict everything that could happen at runtime during compile time. Services go down, APIs change, and so on. When you have a system that can be manipulated at runtime, you can easily adapt to the changes without having any downtimes.

1. 1

That sounds like a good argument for manipulating something at runtime, but not dynamic types. You can build statically-typed platforms that allow runtime inspection or modification. The changes will just be type-checked before being uploaded. The description of StrongTalk comes to mind.

1. 2

Static type systems are typically global, and this places a lot of restrictions on what can be modified at runtime. With a dynamic language you can change any aspect of the running application, while arbitrary eval is problematic for static type systems.

2. 1

When you have a system that can be manipulated at runtime, you can easily adapt to the changes without having any downtimes.

There are architectural choices that address this point, in most situations, better IME. That is, standard setup of load balancer for application servers and something like CARP on the load balancers. For street cred, I’ve worked as an Erlang developer.

1. 1

Sure, you can work around that by adding a lot of complexity to your infrastructure. That doesn’t change the fact that it is a limitation.

1. 1

In my experience, if uptime is really important, the architecture I’m referring to is required anyways to deal with all the forms of failure other than just the code having a bug in it. So, again in my experience, while I agree it is a limitation, it is overall simpler. But this whole static vs dynamic thing is about people willing to accept some limitations for other, perceived, benefits.

1. 1

My experience is that it very much depends. I’ve worked on many different projects, and sometimes such infrastructure was the right solution, and in others it was not. For example, consider the case of the NASA Deep Space 1 mission.

1. 2

I’m not sure how Deep Space 1 suits the point you’re making. Remote Agent on DS1 was mostly formally verified (using SPIN, I believe) and the bug was in the piece of code that was not formally verified.

1. 1

The point is that it was possible to fix tis bug at runtime in a system that could not be load balanced or restarted. In practice, you don’t control the environment, and you simply cannot account for everything that can go wrong at compile time. Maybe your chip gets hit by a cosmic ray, maybe a remote sensor gets damaged, maybe a service you rely on goes down. Being able to change code at runtime is extremely valuable in many situations.

1. 1

The things you listed are accountable for at build time. Certainly NASA doesn’t send chips that are not radiation hardened into space saying “we can just remote debug it”. Sensors getting damaged is expected and expecting services one relies on going down is table stakes for a distributed system. And while I find NASA examples really cool, I do not find them compelling. NASA does a lot of things that a vast majority of developers don’t and probably shouldn’t do. Remember, NASA also formally verifies some of their software components, but you aren’t advocating for that, which makes the NASA example confusing as to which lesson one is supposed to take from it. And those cosmic rays are just as likely to bring down one’s remote debugging facility as it is to break the system’s other components.

1. 1

I think you’re fixating too much on NASA here. The example is just an illustration of the power of having a reloadable system. There are plenty of situations where you’re not NASA and this is an extremely useful feature. If you can’t see the value in it I really don’t know what else to say here really.

1. 1

I’m responding to the example you gave, if you have other examples that are more compelling then I would have expected you to post that.

1. 1

What’s compelling is in in the eye of the beholder. It’s pretty clear that there’s nothing I can say that you will find convincing. Much like I’m not convinced by your position.

1. 2

There was a period of time when I was all about OCaml. I appreciate the purity of Caml and StandardML more though, for whatever reason, just from an aesthetics point (the object-orientedness of OCaml just seems shoehorned in to me).

The sad truth, though, is that in my limited time I have to focus on the stuff I need for work. The only languages I’m truly fluent in anymore are C, Python, SQL, Bourne shell, and…I guess that’s it. I can get around in Lua if I need to, but I haven’t written more than a dozen lines of code in another language in at least five years.

(That’s not to say I don’t love C, Python, SQL, and Bourne shell, because I do.)

I’ve been messing around with Prolog (the first language I ever had a crush on) again just for fun, but I’m worried I’m going to have to put it down because of the aforementioned time issue. Maybe I can start writing some projects at work in ML. :)

1. 7

SML is probably my favorite language. It’s compact enough that you can keep the whole language (and Basis libraries) in your head fairly easily (compared to, say, Haskell, which is a sprawling language). I find strict execution much easier to reason about than lazy, but the functional-by-default nature remains very appealing.

Basically, it’s in a good sweet spot of languages for me.

But, it’s also a dead language. There is a community, but it’s either largely disengaged (busy writing other languages for work), or students who have high engagement but short lifespans. There are a few libraries out there, and some are good but rarely/never updated, and some are not good and rarely/never updated.

I still think it’s a great language to learn, because (as lmmm says) being fluent in SML will make you a better programmer elsewhere. Just know that there aren’t many active resources out there to help you actually write projects and whatnot.

1. 2

Everything that you said, plus one thing: Standard ML, unlike Haskell or OCaml, realistically allows you to prove things about programs — actual programs, not informally described algorithms that programs allegedly implement. Moreoever, this doesn’t need any fancy tools like automatic theorem provers or proof assistants — all you need is simple proof techniques that you learn in an undergraduate course in discrete mathematics and/or data structures and algorithms.

1. 3

Absolutely. I think the niche for languages with a formal specification is fairly small, but it is irreplacable in that niche.

1. 1

Just out of curiosity, do you have any reading recommendations on formal proofs for ML programs?

1. 3

Let me be upfront: When I said “prove” in my previous comment, I didn’t mean “fully formally prove”. The sheer amount of tedious but unenlightening detail contained in a fully formal proof makes this approach prohibitively expensive without mechanical aid. Formal logic does not (and probably cannot) make a distinction between “key ideas” and “routine detail”, which is essential for writing proofs that are actually helpful to human beings to understand.

With that being said, I found Bob Harper’s notes very helpful to get started, especially Section IV, “Programming Techniques”. It is also important to read The Definition of Standard ML at some point to get an idea of the scope of the language’s design, because that tells you what you can or can’t prove about SML programs. For example, the Definition doesn’t mention concurrency except in an appendix with historical commentary. Consequently, to prove things about SML programs that use concurrency, you need a formalization of the specifics of the SML implementation you happen to be using (which, to the best of my knowledge, no existing SML implementation provides).

2. 3

OCaml is yet another mainstream-aiming language full of dirty compromises and even outright design mistakes:

• The types of strict lists, trees, etc. are not really inductive, due to OCaml’s permisiveness w.r.t. what can go on the right-hand side of a let rec definition.
• It has an annoying Common Lisp-like distinction between “shallow” and “deep” equality.
• Moreover, either kind of equality can be used to violate type abstraction.
• Mutation is hardwired into several different language constructs (records, objects), rather than provided as a single abstract data type as it well should be.
• Applicative functors with impure bodies are leaky abstractions.
1. 3

Many complaints about OCaml here are justified in a way (I use it in my day job), so I’ve run into a number of issues myself. It is a complex language, especially the module language.

the object-orientedness of OCaml just seems shoehorned in to me

I think that’s a commonly repeated myth but OCaml OOP is not really like Java. Objects are structural which gives it a quite interesting spin compared to traditional nominal systems, classes are more like templates for objects and the object system is in my opinion not more shoehorned than polymorphic variants (unless you consider those shoehorned as well).

1. 4

…OCaml…(I use it in my day job)

So how’s working at Jane Street? :)

Objects are structural which gives it a quite interesting spin compared to traditional nominal systems…

Oh no, I get that. It’s a matter of having object-oriented constructs at all. It’s like C++ which is procedural and object-oriented, and generic, and functional, and and and. I like my languages single-paradigm, dang it! (I know it’s a silly objection, but I’m sometimes too much of a purist.)

2. 1

I work full-time in Scala, and I credit Paulson with teaching many of the foundations that make me effective in that language. Indeed even when working in Python, my code was greatly improved by my ML experience.

1. 1

How is Scala? I feel like there would be a significant impedance mismatch between the Java standard libraries, with their heavy object-orientation, and Scala with its (from what I understand) functional style.

I think it would also bug me that the vast majority of the documentation for my languages libraries would be written for another language (that is, I need to know how to use something in Scala, but the documentation is all Java).

1. 2

How is Scala?

It’s really nice. More expressive than Python, safer than anything else one could get a job writing.

I feel like there would be a significant impedance mismatch between the Java standard libraries, with their heavy object-orientation, and Scala with its (from what I understand) functional style.

There’s a mismatch but there are libraries at every point along the path, so it gives you a way to get gradually from A to B while remaining productive.

I think it would also bug me that the vast majority of the documentation for my languages libraries would be written for another language (that is, I need to know how to use something in Scala, but the documentation is all Java).

Nowadays there are pure-Scala libraries for most things, you only occasionally have to fall back to the Java “FFI”. It made for a clever way to bootstrap the language, but is mostly unnecessary now.

1. 1

Very informative, thank you.

1. 1

The object-oriented approach, based on the theory of abstract data types, provides a particularly appropriate framework for discussing and enforcing reliability.

The first half of the sentence is false: objects are fundamentally different from abstract data types.

The second half of the sentence requires further qualification, since it is in general not true. For example, both objects and abstract data types have little to offer to implementors of cryptographic algorithms.

It is important to include the preconditions and postconditions as part of the routine declarations.

Clearly, preconditions and postconditions ought to be a part of the routine’s documentation. But it is not clear why they should be a part of the routine itself. For example, Hoare’s and Dijkstra’s formalisms use predicates on the program state to guide the verification and construction of programs, respectively, but these predicates are not a part of the program itself.

Invariants, the next major use of assertions, are unconceivable outside of the object-oriented approach.

Mmm… Okay. (Granted, runtime-checked assertions are not used, but invariants certainly are.)

In some cases, one might want to use quantified expressions (…) by using (…) calls to functions that rely on loops to emulate the quantifiers.

Try quantifying over infinite domains in this way.

The use of functions [read: procedures] — that is to say, computations — is not without its dangers. (…) software functions [read: procedures] can produce side effects (change the state of the computation).

Indeed. Moreover, computation itself is a kind of effect, by virtue of the fact it takes time and uses space. If you take the view that complexity requirements are a part of the functional specification, then the very act of checking assertions can make an otherwise correct procedure incorrect.

any function used in assertions must be of unimpeachable quality

To be unimpeachably assessed how?

What is to prevent a redeclaration from producing an effect that is incompatible with the semantics of the original version? Nothing, of course. No design technique is immune to misuse.

Some design techniques are more prone to misuse than others. For example, while abstract data types can be incorrectly implemented, the invariants of a correctly implemented abstract data type cannot be violated by third parties. This shows that classes are not abstract data types.

But at least it is possible to help serious designers use the technique correctly: here the contract theory provides the proper perspective.

Contracts merely mitigate the damage caused by the ability to arbitrarily redefine features. A simpler alternative is to disallow such redefinitions.

What redeclaration and dynamic binding mean is the ability to subcontract a task

The same effect can be achieved with less semantic complication by manipulating procedures as a first-class values. My apologies for the misnomer in the linked article’s title.

Invariants are always passed on to descendants.

Mmm… Okay.

The contract theory provides a good starting point for a more rational solution. If a routine is seen not just as some “piece of code” but as the implementation of a certain specification — the contract — it is possible to define a notion of failure.

Alternatively, you should only promise what you can actually deliver.

1. 3

The author seems to have no idea what an “algebra” is. From a universal algebra point of view, an algebra consists of a carrier set, and operations of various arities defined on the set. Objects are not algebras. In an object-oriented world, each individual object carries its own operations. Algebras correspond much more closely to abstract data types, as even proponents of object-orientation acknowledge.

1. 2

Whenever I see CL’s condition system it seems to me that we could achieve the same effect by passing handlers as lambdas to a computation. Or, in the case of an OO language, creating an object for the computation and parameterizing its construction with strategy objects as the handlers.

Then, I wonder why people don’t do either of those that often.

1. 3

Then, I wonder why people don’t do either of those that often.

Because it’s a frigging lot of work. And also because eventually a user will want a hook that you didn’t provide, or a hook with a different shape from the one you provided, and then refactoring your code to accomodate their use case will cause you a world of pain.

The solution as a library author is to say no to inversion of control, and write first-order procedures that do one simple thing at a time. Whenever you would normally use a higher-order procedure (aka “higher-order functions” or “methods taking strategy arguments”), do the following instead:

• Identify the points at which the higher-order procedure calls a procedure argument.
• Reify the state of at those points as custom data structures.
• Instead of calling a procedure argument, return the current state immediately.
• Write another procedure that resumes the continuation with the result of the procedure argument.

This gives your users the freedom to handle the continuation however they want, without force-fitting square pegs into round holes. I am firmly convinced now that the only legitimate use case for first-class procedures is implementing custom control flow, e.g., laziness and concurrency.

1. 2

I had a hard time understanding the Matt Might paper, but his lecture on it really helped me. He also motivates it really well.

1. 1

Somewhere around the 40 minute mark, those definitions of D and δ using define/memoize and define/fix really made my day. :-)

1. 7

Some Haskell features are just mistakes; others are designed for PL researchers to experiment, but their usefulness in industrial programming is yet to be proven.

I’d like to see a list of which Haskell features aren’t considered good for production code, and why! I’ve decided TransformListComp is one, because it has zero uptake in the community. Years ago I saw ImplicitParams go horribly wrong, but haven’t tried it since.

Got any features you feel are good or bad for production Haskell?

1. 2

This is a good start on an answer: https://stackoverflow.com/a/10849782/108359

1. 0

Lazy evaluation makes it hard to reason about the space usage or even termination of a program. I prefer having eager evaluation with lazy data structures.

1. 8

The downside is that you can’t use functions for control flow. An obvious example is Church encoding, e.g.

true x y = x
false x y = y
ifThenElse c x y = c x y


If we call ifThenElse eagerly, both branches x and y will be calculated; if we used these to e.g. select between a base case and a recursive case, we’d cause an infinite loop.

Most eager languages resort to a built-in lazy if construct (Haskell has one too, but it’s unnecessary), which forces us to reframe our problem in terms of some built-in boolean type rather than custom domain-specific types (for a similar issue, see boolean blindness).

On the one hand, (Church) booleans are quite a weak argument for laziness since “real programs” will be using some richer, more meaningful, custom datatypes instead; yet on the other hand, most eager programs end up relying on booleans, since they’re the only thing that works with the built-in if!

Whilst an eager language with things like case and pattern-matching can alleviate some of these problems, I still think that lazy function calls are important. In fact, I think this is a blub paradox, since even eagerly evaluated languages provide lazy && and || functions; but again, this is usually limited to hard-coded, built-in constructs.

1. 4

The lazy if example always stroke me as silly. It is actually less elegant than you might think: to call it, you need to create two thunks, even though you know in advance that (at least) one will be discarded. I know that optimizing compilers can get rid of the overhead, but that would be an implementation detail that isn’t immediately justified by the semantics of the language in question. In any case, you don’t need if as a built-in in a strict language. It is nothing but syntactic sugar for pattern matching on Bool. Similarly, arithmetic if is syntactic sugar for pattern matching on an Ord produced by a call to compare. Etc. etc. etc.

By making a sharp distinction between values and computations, strict languages gain expressivity over lazy ones. If you want to recover the benefits of laziness in a predominantly strict language, you can always define an abstract type constructor of thunked computations - that can be implemented in 20-30 lines of ML. On the other hand, adding seq to a lazy language wreaks havoc in its semantics, weakening or destroying many free theorems, presumably the main reason for preferring a lazy language over a strict one.

1. 3

In any case, you don’t need if as a built-in in a strict language. It is nothing but syntactic sugar for pattern matching on Bool. Similarly, arithmetic if is syntactic sugar for pattern matching on an Ord produced by a call to compare. Etc. etc. etc.

Yes, I hand-waved this away as “things like case and pattern-matching” :)

a sharp distinction between values and computations

From this perspective, my point could be phrased as laziness “unifying” values and computations. In the if example, we can implement it eagerly by making the thunks explicit, e.g. giving true and false type (Unit -> a) -> (Unit -> a) -> a. Or should that be (Unit -> a) -> (Unit -> a) -> Unit -> a? Maybe we need both…

One of my favourite things about programming is when I come across unifications of concepts I’d previously considered separate. Examples which come to mind are Python classes being first-class objects, Smalltalk control-flow statements (e.g. ifTrue:) being method calls, Lisp code being data (in a way that’s both useful (unlike strings) and looks the same unlike complicated AST encodings), and pointers being ints in C.

Whilst I accept that we may lose expressivity, and this can certainly be important for resource-constrained or -intensive tasks, for the sorts of inefficient plumbing I tend to write I very much like the symmetry that is gained from having fewer distinct concepts/constructs/etc. to take into account (especially when meta-programming!).

adding seq to a lazy language wreaks havoc in its semantics, weakening or destroying many free theorems

That’s certainly a problem, I agree :(

1. 4

Yes, I hand-waved this away as “things like case and pattern-matching” :)

Handwaving is failing to provide a proof. What you did was simply make a wrong statement:

Whilst an eager language with things like case and pattern-matching can alleviate some of these problems, I still think that lazy function calls are important.

Pattern matching isn’t there to “alleviate” any “problems” caused by the lack of laziness. Pattern matching is the eliminator for sum types, which, by the way, don’t actually exist in lazy languages.

since even eagerly evaluated languages provide lazy && and || functions; but again, this is usually limited to hard-coded, built-in constructs.

In a strict language, && and || are not functions, but rather syntactic sugar over nested uses of pattern matching on the boolean type.

From this perspective, my point could be phrased as laziness “unifying” values and computations.

You aren’t unifying anything. What you’re doing is ditching values altogether, and replacing them with trivial computations that return those values. In your limited world, values only exist “at the end of the computation”, but they are not first-class mathematical objects that you can, say, bind to variables. So you are deprived of any proof techniques that rely on variables standing for values, such as structural induction.

On the other hand, if you properly place value types and computation types in separate categories, you will find that these categories are related by an adjunction and admit different universal constructions. Explicitly acknowledging this structure allows you to define abstractions that don’t break in the face of nontermination or explicit thunk-forcing, unlike most of Haskell’s library ecosystem.

One of my favourite things about programming is when I come across unifications of concepts I’d previously considered separate.

If essential properties of the objects being “unified” are lost, it stops being “unification” and becomes “conflation”.

for the sorts of inefficient plumbing I tend to write I very much like the symmetry that is gained from having fewer distinct concepts/constructs/etc. to take into account (especially when meta-programming!).

If anything, you have destroyed the symmetry (duality) between values and computations.

1. 3

Pattern matching isn’t there to “alleviate” any “problems” caused by the lack of laziness. Pattern matching is the eliminator for sum types

Elimination is when we select one of the branches. That can be done before or after evaluating them. That’s the distinction I was making: in my made-up terminology an “eager case expression” would evaluate all branches to normal form, then select the appropriate one to return; a “lazy case expression” would select the appropriate branch before attempting to evaluate any of the branches. You’re right that if, && and || in eager languages are syntactic sugar over pattern matching (case), but my point was that even eager languages use the “lazy case expression” variety, not the “eager case expression”.

The way those languages achieve such laziness is by making pattern-matching a special language construct. We can’t write user functions which behave the same way (unless we distinguish between values and thunks); note that we can write macros to do this, as is common in Lisps.

With lazy function calls, such “lazy case expressions” can, in principle, be replaced by eliminator functions (like Church encodings and their variants); although I currently think that would be less nice (see Morte and Dhall, for example).

If essential properties of the objects being “unified” are lost, it stops being “unification” and becomes “conflation”.

Sure, but what counts as “essential” is subjective. C programmers might consider pointer arithmetic to be essential, which is lost by high-level representations like algebraic (co-)datatypes. Personally, I’m perfectly happy to e.g. conflate scope with lifetime (i.e. garbage collectors based on liveness).

I don’t have particularly strong opinions when it comes to either distinguishing or conflating the distinctions used by CBPV, “polarity”, co/data, etc. That’s why I currently fall back on my “symmetry” heuristic.

If anything, you have destroyed the symmetry (duality) between values and computations.

By “symmetry” I didn’t mean “duality between two different sorts of thing”, I meant “treating all of these things in a single, uniform way” (i.e. conflating). Fewer distinctions means fewer choices to be made, fewer cases to be handled and fewer combinatorial explosions to tackle. This makes life easier when e.g. parsing, code-generating, interpreting, etc.

Of course, conflating is a simplistic thing to do; yet such ease is nice to have, so I treat it as the “activation energy” (the ease/value offered) that each distinction must overcome in order for me to use them (at the loss of symmetry).

Examples of distinctions which I think are generally worth it (for me):

• Type-level/value-level (as found in dependently-typed languages)
• Compile-time/run-time
• Pure/effectful

Distinctions I don’t think are worth it (for me):

• Type-level/kind-level
• Separate constructs for types/values (e.g. type-level computation in Haskell, type families, etc.)
• Statements/expressions
• Linear/non-linear types
• Concrete/abstract syntax (i.e. not using s-expressions)
• Value/delayed-computation (“polarity”)
• Partial/total
• Native/managed

Of course, these are just my preferences, and they vary depending on what problem I’m tackling and what mood I’m in ;)

1. 3

Elimination is when we select one of the branches. That can be done before or after evaluating them. That’s the distinction I was making: in my made-up terminology an “eager case expression” would evaluate all branches to normal form

This doesn’t make sense. Expressions under binders are not reduced in a call-by-value language, and the left-hand side of a branchn is very much a binder for any variables used as constructor arguments. So what you call “eager case expression” does not exist at all.

The way those languages achieve such laziness is by making pattern-matching a special language construct.

A strict language with pattern matching doesn’t “achieve laziness”. It simply evaluates arms at the correct moment.

Sure, but what counts as “essential” is subjective. C programmers might consider pointer arithmetic to be essential, which is lost by high-level representations like algebraic (co-)datatypes.

I’m not sure pointer arithmetic is essential, but array manipulation certainly is essential, and memory-safe languages do a very poor job of dealing with it. I’d be willing to give up memory-safety in exchange for a predicate transformer semantics for array manipulation, so long as the semantics is explicitly formalized.

Personally, I’m perfectly happy to e.g. conflate scope with lifetime (i.e. garbage collectors based on liveness).

I’m not. Languages without substructural types suck at manipulating anything that doesn’t last forever (e.g., file handles).

(i.e. conflating). Fewer distinctions means fewer choices to be made, fewer cases to be handled and fewer combinatorial explosions to tackle. This makes life easier when e.g. parsing, code-generating, interpreting, etc.

And it makes life harder when debugging. Not to mention when you want to formally prove your programs correct. (I do.)

1. 2

Expressions under binders are not reduced in a call-by-value language

Yes, that’s what I’m referring to as ‘a form of laziness’. Expressions under binders could be (partially) reduced, if we wanted to. Supercompilers do this (at compile time), as do the morte and dhall languages, for example.

what you call “eager case expression” does not exist at all

The reason that basically no language does this is because it’s a pretty terrible idea, not that it couldn’t be done in principle. It’s a terrible idea because it evaluates things which will be discarded, it introduces preventable non-termination (e.g. with base/recursive cases), and seems to have no upsides.

My point is that the same can be said for strict function calls, apart from the “no upsides” part (upsides of strict calls include preventing space leaks, timely release of resources, etc.).

array manipulation certainly is essential… I’d be willing to give up memory-safety… Languages without substructural types suck… makes life harder when debugging… when you want to formally prove your programs correct

I think this is where our priorities differ. I’m happy enough with an inefficient, simple(istic) language, where I can formally reason about “getting the right answer (value)”, but I don’t care so much about how we arrive there (e.g. order of evaluation, space usage, garbage collection, etc.)

1. 4

Expressions under binders could be (partially) reduced, if we wanted to. (…) The reason that basically no language does this is because it’s a pretty terrible idea, not that it couldn’t be done in principle.

Sure, but not in a call-by-value language. The distinguishing feature (a killer feature!) of call-by-value languages is that variables stand for values, which is not true if expressions are reduced under binders.

Supercompilers do this (at compile time), as do the morte and dhall languages, for example.

Except for simple cases where the program’s asymptotic time and space costs are not altered, this is a terrible idea. (Yes, even when the program’s performance is improved!) I want to reason about the performance of my program in terms of the language I am using, not whatever machine or intermediate code a language implementation could translate it into. The former is my responsibility, the latter is beyond my control.

2. 5

Lazy evaluation makes it hard to reason about the … termination of a program

A program terminates at least as quickly when evaluated non-strictly as it terminates when evaluated strictly, so that can’t be true.

1. 3

For once I second @Yogthos. Lazy evaluation is certainly useful, but not as the default! If you care about algorithms, and IMO every programmer ought to, strict evaluation as the default makes analysis easier than lazy evaluation (“simply substitute and reduce” vs. “keep track of which thunks have been forced”) and gives tighter asymptotic bounds (worst-case vs. amortized) on running times.

1. 4

Strict evaluation should not be the default, you lose composition of algorithms.

1. 2

Eta-expand, then compose. Voilà.

1. 1

Eta-expand then compose what?

1. 3

For instance, rather than say foo . bar, where foo and bar are arbitrarily complicated expressions, you say \x -> foo (bar x).

As for composing complicated algorithms - it’s totally overrated. Instead of designing libraries around a mess of higher-order functions, oops, Kleisli arrows, oops, profunctors, oops, who knows, I’d rather reify every intermediate state of a complex operation using a custom abstract data type, and then only export procedures that perform individual atomic steps - good old-fashioned first-order procedures! Composing these atomic steps into the exact algorithm the user wants is best done by the user himself. Maximum flexibility and no abstraction overhead. But of course, you need decent support for abstract data types for this to work.

1. 4

I also have to do that for everything in foo and bar, then manually fuse -> code duplication.

2. 2

Perhaps the issue is less direct: laziness tempts us to use infinite (co)datastructures, which we must handle carefully (e.g. don’t take the length of an infinite list).

1. 1

Correction: I should have said “when evaluated lazily” not “non-strictly”. I think as written what I said was false.

2. 2

By the way, that’s not really what Shapr meant by “which Haskell features aren’t considered good for production code”!

1. 6

It hasn’t improved much IMO.

Haskell is normally extremely strong when it comes to well-designed and reusable abstractions. Unfortunately that appears to be more or less absent from the Haskell crypto libraries. There are a few different monad classes for pseudorandom number generation, for example, and all of them are overcomplicated. I often end up just rolling my own (monad, not PRNG) when I need clean random number generation.

There are a few decent libraries available for sundry concrete cryptographic tasks, but well below par for the Haskell ecosystem.

In fairness, cryptography libraries are bad across almost all languages, but I expect more from Haskell.

1. 4

Is it fair to suggest that Haskell expects more from you, too? I mean, you’re certainly welcome to contribute.

1. 3

In fairness, cryptography libraries are bad across almost all languages, but I expect more from Haskell.

Why? Does Haskell have any special features that make it fundamentally easier to correctly implement cryptography algorithms compared to other high-level languages? Parametricity doesn’t particularly help when all your routines map tuples of integers to tuples of integers.

1. 4

Does Haskell have any special features that make it fundamentally easier to correctly implement cryptography algorithms compared to other high-level languages?

Yes, e.g. QuickCheck, QuickSpec, LiquidHaskell, etc.

1. 4

These get you some of the way but there’s a whole class of dude channel attacks we have very little ability to reason about in Haskell. Timing is something I have no idea how to talk about how to make a constant time Integrr multiplication algorithm and be sure it is constant time.

My dream for this sort of work is a inline-rust package, in the vain of inline-c, so we get memory safety but also a language which better allows timing analysis.

1. 2

inline-rust is something I want in every programming language. :)

I think it’s possible that a subset of Haskell in which you only use primitive types and primops (like Word32# and MutableByteArray# and so on) and can’t have any laziness anywhere (because no values are ever boxed) might be more amenable to timing analysis.

I’m not sure if there is a pragma or Language setting in GHC that can automatically enforce that everything in a given file uses only primitives and primops.

1. 2

Check out Jasmin for language implementing high-assurance crypto. Once again, it’s achieved with a language quite opposite of Haskell’s high-level style.

1. 2

That would be cool indeed—but I can already viscerally imagine the impact on build times from invoking the Rust compiler via Template Haskell… :)

2. 3

In 2017, QuickCheck is by no means specific to Haskell. Nowadays you can find property-based testing libraries and frameworks for just about any language.

As for LiquidHaskell, the real verification is performed by an external SMT solver. So again I don’t think this constitutes a Haskell-specific advantage.

3. 3

Because Haskell libraries are, in general, much higher quality than libraries in other ecosystems I use. Correctness also isn’t the concern — I have little doubt that the crypto libraries are correct. The concern is usability. Most of the Haskell crypto libraries are clumsy, typically because they just wrap some C library without providing any additional abstractions.

1. 2

So you are confident the underlying C library is correct?

1. 5

Here are some reasons for not loving Ada:

• It is not type safe, even if you only use features that were meant to be type safe. In other words, Ada’s type system fails at being a type system. “Almost safe” languages (Ada, Eiffel, etc.) are actually more dangerous than C, since at least C programmers are permanently aware that they are walking through a semantic minefield, whereas users of “almost safe” languages often think they aren’t.

• Much of Ada’s type system exists to automate the insertion of runtime safety checks, just like much of pre-templates C++’s type system exists to automate the insertion of runtime type coercions and cleanup operations. Now, automation is nice, but, are types the right tool for this job? I do not think so. Macros offer a more compelling alternative.

• With Ada, you can pick at most two between safety, efficiency and an implementation-independent semantics. Safely getting rid of the onerous runtime checks requires external analyses not evidently justified by the Ada specification. A formal semantics for the whole of Ada (not just the subset without dynamic resource management) is very much missing.

1. 5

at least C programmers are permanently aware that they are walking through a semantic minefield, whereas users of “almost safe” languages often think they aren’t.

This is a very good point, and in my experience it also applies to functional purity. In an inherently impure language like C or Java, you’re always aware that shared mutable state is present and consequently you’re on guard for it, so you generally won’t build abstractions that depend on purity in order to work. In a language like Haskell or Elm, on the other hand, you know that the compiler actually offers strong purity guarantees at the type level, so you can use functional abstractions on a large scale with confidence. The real problem lies in the middle, when you’re using a language or a library that is pure by convention but will accept impure functions as well, and you build functional abstractions on it that break in really subtle and unexpected ways when mutability and nondeterminism come into play. I’d say an example of the latter category is some modern JS frameworks like React, which depend heavily on the programmer keeping track of what subset of their code has to be pure and what subset can be imperative, all in a language that has no compile-time ability to distinguish the two.

1. 2

It is not type safe, even if you only use features that were meant to be type safe. In other words, Ada’s type system fails at being a type system. “Almost safe” languages (Ada, Eiffel, etc.) are actually more dangerous than C, since at least C programmers are permanently aware that they are walking through a semantic minefield, whereas users of “almost safe” languages often think they aren’t.

That example doesn’t support the point because it’s using an Unchecked package, which exist solely to side step the type system. They’re the Ada equivalents of Haskell’s Unsafe functions.

Much of Ada’s type system exists to automate the insertion of runtime safety checks, just like much of pre-templates C++’s type system exists to automate the insertion of runtime type coercions and cleanup operations. Now, automation is nice, but, are types the right tool for this job? I do not think so. Macros offer a more compelling alternative.

I don’t think I agree with the premise that Ada’s type system exists to automate the insertion of runtime safety checks. It can be viewed in that way, but so can any other type system. In reality, an Ada compiler is free to skip any runtime check that it can detect is unnecessary.

1. 2

That example doesn’t support the point because it’s using an Unchecked package, which exist solely to side step the type system.

Re-read the code. The Conversion function doesn’t use anything from any Unchecked package. The Unchecked_Conversion function is only imported for comparison purposes.

It can be viewed in that way, but so can any other type system.

That would be wrong. For certain type systems, e.g. ML’s, it is a theorem that legal programs can be striped of all type information without altering the dynamic semantics of the language.

In reality, an Ada compiler is free to skip any runtime check that it can detect is unnecessary.

Yes, but it is in general undecidable whether a specific check can be safely elided. Things wouldn’t be so bad with a formal semantics for Ada, allowing programmers to verify by themselves that specific checks can be safely elided.

EDIT: Fixed identifier. Added last sentence.

2. 2

I would like to add another reason: not much choice between implementations of Ada.

1. 2

This one doesn’t bother me at all, although I can see why others would consider it a problem.

1. 5

See also ‘maximizers and satisficers’. I wrote something about that aspect of this question a while back:

https://journal.dedasys.com/2006/02/18/maximizers-satisficers-and-programming-languages/

1. 3

if your goal is simply to accomplish some task, rather than spending too much time fretting about finding the perfect tools to accomplish the task with.

To a maximizer, it’s not about finding the perfect tool to perform a task. It’s about finding the Right Way™ to do it. Rob Pike truly nails it when he says:

C++ programmers don’t come to Go because they have fought hard to gain exquisite control of their programming domain, and don’t want to surrender any of it. To them, software isn’t just about getting the job done, it’s about doing it a certain way.

For example, Stepanov is a maximizer:

STL, at least for me, represents the only way programming is possible. It is, indeed, quite different from C++ programming as it was presented and still is presented in most textbooks. But, you see, I was not trying to program in C++, I was trying to find the right way to deal with software.

In some instances, actually reducing people’s choices makes them happier. Python’s “one good way to do it” makes everyone happy, because both maximizers and satisficers know that they’re doing things right, and don’t have room to worry.

To a maximizer, this is only as good as the extent to which they agree with the “one good way to do it” that Python suggests. Otherwise, they will have a lot to worry about.

1. 1

Great presentation. Far as application, I already thought this might be useful in lightweight, formal methods to spot problems and suggest corrections for failures in Rust’s borrow checkers, separation logic on C programs, proof tactics, and static analysis tooling. For Rust example, the person might try to express a solution in the language that fails the borrow checker. If they can’t understand why, they submit it to the system that attempts to spot where the problem is. The system might start with humans spotting it and restructuring the code to pass borrow checker. Every instance of those will feed into the learning system that might eventually do that on its own. There’s also potential to use automated, equivalence checks/tests between user-submitted code and the AI’s suggestions to help human-in-the-loop decide if it’s worth review before passing onto the other person.

(@manishearth @steveklabnik what do you think about the deep learning vs borrow checker idea? Are the troubles you two see across the different uses of borrow checker similar looking enough to possibly be worth attempting that project? It would seem effective if humans already have an intuitive sense for structures to avoid or use as machines can probably find those.)

In hardware, both digital and analog designers seem to use lots of heuristics in how they design things. Certainly could help there. Might be especially useful in analog due to small number of experienced engineers available.

1. 3

failures in Rust’s borrow checkers

There is only one.

The system might start with humans spotting [the problem] and restructuring the code to pass [the] borrow checker. Every instance of those will feed into the learning system that might eventually do that on its own.

DWIM was never a good idea. How can you trust a programming system that replaces the program you wrote (however incorrect it might be) with another program that has a completely different meaning? Are you willing to take responsibility for the program the tool wrote? If not, who will? As you know, tools are not sentient, and thus cannot take responsbiility for anything.

The borrow checker exposes the complexity of writing programs that manipulate ephemeral resources, and of course this causes pain. However, sweeping these problems under the carpet won’t fix anything. There is no way around actually learning to program.

1. 1

Are you willing to take responsibility for the program the tool wrote?

It’s a suggestion that should be checked for equivalence and comprehension by the developer. If it solved the problem, they should learn from it. If this becomes a panacea, they’ll just run into problems constantly. That passing borrow check is a basic requirement of Rust code in production should (theoretically) encourage them to use the support tool as training wheels until they learn to ride on their own. It shouldn’t substitute for that.

However, with separation logic or some things in proof, it’s clear reading the literature that a lot of trouble is just in weaknesses of the tooling. Better tactics often automatically find what was manual before. If the spec and algorithm were decent, then a good chunk of that is really mundane stuff that should get automated. Still done with human review of specs for errors and a trusted checker so proof tactics can be untrusted.

1. 4

It’s a suggestion that should be checked for equivalence

The tool you propose replaces an illegal program with a legal one. However:

• Under a typeless (Curry-style) semantics for Rust, an illegal program may have undefined behavior, whereas a legal program definitely does not. So a legal program semantically equivalent to the original illegal one could well not exist.

• Under a typeful (Church-style) semantics for Rust, an illegal program is not a program to begin with, so a semantically equivalent legal program definitely does not exist.

So there are no grounds for talking about program equivalences.

and comprehension by the developer.

There exist three kinds of programmers:

• Those who do not understand ownership and borrowing, and hence will not be able to make heads or tails of the suggestion made by the tool you propose. (Assuming that a meaningful suggestion can be made to begin with, which is not always the case, as shown above.)

• Those who understand how ownership and borrowing work in Rust, and hence don’t need the tool you propose.

• Those who understand ownership and borrowing, but not how they work in Rust. What they need to learn is how to express what they already understand using Rust’s syntax, and this is relatively easy task, so they probably have little use for the tool you propose as well.

However, with separation logic or some things in proof, it’s clear reading the literature that a lot of trouble is just in weaknesses of the tooling.

By far the most important problem is that coming up with a correct program is hard. This cannot be fixed with tooling. Rust is merely a language in which some of the difficulties involved in coming up with a correct program can be expressed and verifiably avoided.

1. 4

In order to compare learned indexes with B-Trees, we created 4 secondary indexes over 3 real-world datasets: (1) Weblogs, (2) Maps, and (3) web-documents (…) [numbering not mine]

A more real use case for B-trees is ERP systems. If learned indices can handle the transactional volume of an ERP system better than B-trees, then maybe DBMS implementors should start paying attention…

1. 2

If we’re going to revive this, maybe I should start a pointless and interminable dispute. Like, “Lisp isn’t a functional language” or “C++/Java/C# isn’t object-oriented” or similar.

(Both of those have been seriously defended, BTW, and by people of importance.)

We can turn this around, ask whether Dylan is a Lisp, or whether Python is a Lisp. Hell, by some measures, Lisp won the Programming Wars when nobody was looking, and now it’s just Java and C++ and Rust picking up the scraps far away from where the action is.

1. 4

Go for it. More fuel for the fire.

Whether X is a lisp or not is helpful only with context: Are you saying that it can trace its lineage directly to LISP? Are you saying it’s got cons? (Dylan calls it pair!). Is it’s source code made up of atoms and lists? Does it have macros? Eval and lambda? What exactly is someone trying to say when they say this?

Kent Pitman helped define Common Lisp and he says he agrees with Erik Naggum: “X is a lisp” is worthless. It says nothing about the communities, the underlying representation, the source code lineage, the kinds of functions and capabilities you’ll find, and so on. You still might say it to be polite, or with sufficient context (X is lispy in that it Y), but that’s about it.

1. 3

Hell, by some measures, Lisp won the Programming Wars when nobody was looking

if you consider that JavaScript was inspired & based of Scheme, then Scheme won by a landslide.

1. 7

If this is victory, then some horrible prices must have been paid along the way…

1. 4

Scheme’s biggest innovations w.r.t. Lisp were:

• Proper lexical scope.
• Hygienic macros.

JavaScript has neither.

1. 2

This sounds as if JavaScript was designed after Scheme. To me it seems, that JavaScript kind of “happened”, more by chance and under time pressure. So the inspiration was really more the certainty that a dynamically typed scripting language could work. It was not a concious design decision to take features A, B, C from Scheme, but omit feature D.

2. 3

whether Python is a Lisp

Peter Norvig does say that “Python can be seen as a dialect of Lisp with ‘traditional’ syntax”, although it’s not clear he means that as a particularly strong statement vs an offhand comment about some resemblances. His introduction to Python for Lisp programmers is interesting though.

1. 5

When he finished Peter [Norvig] took questions and to my surprise called first on the rumpled old guy who had wandered in just before the talk began and eased himself into a chair just across the aisle from me and a few rows up.

This guy had wild white hair and a scraggly white beard and looked hopelessly lost as if he had gotten separated from the tour group and wandered in mostly to rest his feet and just a little to see what we were all up to. My first thought was that he would be terribly disappointed by our bizarre topic and my second thought was that he would be about the right age, Stanford is just down the road, I think he is still at Stanford – could it be?

“Yes, John?” Peter said.

I won’t pretend to remember Lisp inventor John McCarthy’s exact words which is odd because there were only about ten but he simply asked if Python could gracefully manipulate Python code as data.

“No, John, it can’t,” said Peter and nothing more, graciously assenting to the professor’s critique, and McCarthy said no more though Peter waited a moment to see if he would and in the silence a thousand words were said.

source

1. 5

Whenever Norvig is quoted that way, there are people quickly pointing out how Python cannot be a Lisp, because of X, Y and Z. Nevertheless, Norvig’s argument is not ticking off a list of necessary features of a language being a Lisp. Rather, it’s about how a typical program looks like. And a typical lisp program is suprisingly imperative, especially if seen through the eyes of someone who is interested in functional programming in 2017. There are loops, occasional recursion, classes and instances, getters and setters, hash-tables and lists.

Macros were probably as popular in the Common Lisp community as writing “decorators” and metaclasses in Python today, it’s something you do rather rarely. I wanted to dig up some reference for this claim, because when I first heard it, I was kind of surprised (being constantly told how great macros in lisp are), so the C2 Wiki has an entry about this: http://wiki.c2.com/?LispMacro

I would put it more strongly. Always use functions, period. In the Lisp community, typically it is not the case that application programmers use macros. It is usually avoided and discouraged. But sometimes you really, really need one, and you then seek out the macro programmer in the group and ask them to provide one that is then available to everyone.

It is the year 2017 and Lisp is almost irrelevant as a platform to write new software in. In a way, it is a fantasy land that we all can project our long-held wishes into. The past we see in our nostalgic dreams, probably never existed in the way we think.

1. 2

And a typical lisp program is suprisingly imperative, especially if seen through the eyes of someone who is interested in functional programming in 2017.

It’s not so surprising. Pick two general-purpose languages: a dynamically typed imperative one and a statically typed functional one. You will find that (Common) Lisp is closer in spirit to the former than to the latter. Lisp and Lisp programmers consistently prefer introspection over abstraction, expressivity over guarantees, and flexibility over sharp distinctions, exactly like other dynamically typed imperative languages and their users.

EDIT: Phrasing.

2. 1

Norvig does admit that in the above article, yeah; see point 11 under “Gotchas for Lisp Programmers in Python”. Lisp has historically had a pretty wide range of programming styles, though, and Python suits some of them in a way that, say, previous competitors like Fortran or Java were completely unsuited for, while it remains unsuitable for other styles.

1. 0

at least the outcome of integer maths is always defined.

Integer arithmetic is well-defined. However, machine integers are not a model of the integers, and what C calls “signed integers” are not a model of anything nice.

if I have complete test coverage then I do not need a type system.

You need to prove your code correct anyway. Test suites merely prevent you from wasting your time trying to prove incorrect code correct.

if I have a type system then I do not need complete test coverage.

You need to prove your code correct anyway. Type systems merely write somewhere between 0.01% and 0.1% of the proof for you.

if the problem is SQL Injection, then the solution is to replace SQL; NoSQL Injection is impossible.

The actual problem is representing queries as strings. Switching to a NoSQL database doesn’t automatically fix that.

… but all of this is basic CS.

1. 4

Using concurrency control tools (channels) to traverse an immutable (or exclusively owned) data structure is using a bazooka to kill a mosquito.

1. 4

In terms of selecting an appropriate vocabulary for discussion or writing, it is imperative to understand your audience. “Bigger” words or technical language often exist to communicate ones ideas more fully and exist as useful abstractions in the right context. The author’s concerns are valid, but it is also worth not limiting yourself to the most simple forms of programming or communication as an absolute rule.

Higher level languages and techniques are inherently more complex, but the benefit of this abstraction is being able to focus on solving a problem by communicating your intent in terms that more closely match your understanding of the problem.

The term “simple” can also mean a lot of different things. C and Ruby are both simple in some ways and complex in others.

1. 3

Higher level languages and techniques are inherently more complex

No. The implementation of high-level languages on machines designed to run Fortran and C might be involved, but their semantics of high-level languages can be quite simple, actually. Not that simple low-level languages cannot possibly exist, of course.

1. 2

Completely agree. My perspective is very biased towards current implementations of high level languages on top of machines designed to be operated at a lower level.

2. 2

The term “simple” can also mean a lot of different things. C and Ruby are both simple in some ways and complex in others.

C is simple, while Ruby is easy… is what I wanted to write immediately after reading last paragraph - which might just prove your point ;)

1. 1

If this is a reference to the well known Rich Hickey talk “Simple Made Easy”, which nails down the definition of simple to something more objective and less squishy than its normal usage, then neither C nor Ruby would be simple in that sense.

Are either of them easy? Well, how familiar are you with them? At one point during college o had written so much C for different systems classes that it was easy. Now, no way. In this sense, simple is an intimrinstic property of the design, ease is a property of the subject answering (in this case, me).

1. 1

Rich Hickey does not give a technically precise definition of “simple”. I have in the past proposed two measures of simplicity:

• The size of a formal semantics for the language in question.
• The size of the proofs of correctness for benchmark programs written in the language in question.

But most other people were at best indifferent to my suggestion. At worst they were made very angry.

EDIT: Fixed typo.

1. 1

I can see both your point and some other peoples’ objections.

For the record, I didn’t say technically precise. His definition is more philosophically or conceptually well founded, if you want me to get specific. It won’t give a snippet of code or a program a “complexity score”, but it is useful for reasoning how relatively complex/simple two concepts, approaches, or solutions are.

And that’s a big improvement over “I feel like closures are complex”, “oh yeah well I feel like they’re simple!”.

Falling short of full technical precision does not delegitimize the his definition, or the conversations that can be had using that definition.

1. 1

I can see both your point and some other peoples’ objections.

I can see their objections too: “How dare you! A formal semantics would expose the complexity of what I’m trying to sell as simple! You damn little…!”

His definition is more philosophically or conceptually well founded, if you want me to get specific.

Philosophy is useful when it guides technical work, but it’s the latter that ultimately we need to get done. If “simplicity” is to become a software quality criterion, we need to abstract, quantify and measure it.

Falling short of full technical precision does not delegitimize the his definition, or the conversations that can be had using that definition.

Without a formal definition, his idea of “simplicity” is just a proxy for his aesthetics.