If You're Not Writing a Program, Don't Use a Programming Language [video]
youtube.com
youtube.com
Honestly I think it might be time to phase out teaching imperative and object-oriented programming. Most of the grief in my career has come from them. I don't care if they're where the jobs are. The mental cost of tracing through highly-imperative code, especially the new implicit style of languages and frameworks like Ruby and AngularJS (which have logic flows having no obvious connection to one another, or transition through async handlers connected by a convention which isn't immediately obvious to the developer) is so high that the underlying business logic is effectively obfuscated.
I think we should get back to fundamentals. Maybe start with the shell and explain why separate address spaces connected by pipes are such a powerful abstraction, maybe touch on the Actor model, maybe show how spreadsheets and functional programming are equivalent, and how even written notation is superfluous. Really focus on declarative programming and code as media, and how that made the web approachable by nontechnical folks before it was turned into single page application spaghetti. There are so many examples from history of where better ways were found before the mainstream fell back into bad habits.
I think the problem with Object-oriented programming is it's taught to soon. Start with Imperative then Functional then toss object oriented into your senior year.
"Computer Science is no more about computers than astronomy is about telescopes." — (Mis)attributed to Edsger Dijkstra, 1970.
Edsger W Dijkstra. Mathematicians and computing scientists: The cultural gap. Abacus, 4(4): 26–31, June 1987. ISSN 0724-6722. URL http://dl.acm.org/citation.cfm?id=25596.25598.
Which is similar in spirit to the contested quote, and predates by a few years any of the references on Wikiquote.
They explain it by explaining the origins of the word 'Geometry', which translates to 'Earth Measurement'. What they deduce is when a field is young, its hard to make a distinction between the science behind the field and instruments/tools you spend time with to make the science happen. That is because you spend so much time with the tools that the big part of the work is tool expertise itself.
Until we arrive at the perfect computers and perfect languages, we are going to be stuck with this sort of a phenomenon for a very long time.
It is also the official term for computer science in many cultures. Mostly in European countries/languages.
Unfortunately, real programs run on real computers and engineers need to deal with that. In theory, theory and practice are the same. In practice, they are not.
I learned to program using BASIC on an Apple II. All of the variables were global, and it wasn't until I got Apple Pascal that I had access to a language that had local variables. I immediately saw the advantage of the discipline of using local variables whenever possible because I had experienced the difficulty of tracking down where in the whole program a global variable might be changed.
It could be argued that local variables are just syntactic sugar over a global memory space, but no one credibly argues today that we should therefore only use global variables. Local variables make it easier to reason about the behavior of a program, and it appears to me that functional programming takes that idea even further.
I am very pro functional programming, but your mental model needs to be accurate to really dig into the details. As such you really need to understand ASM and procedural code or it will eventually bite you.
But that's all just nit-picking <<1% cases. When's the last time you saw a functional program whose execution time or memory footprint were unacceptable, and required knowledge of assembly language (or lower) to resolve? I can't say I ever have.
I don't expect everyone to proficient in ASM let alone microcode, but I do expect them to at least understand that they exist. Beyond that I expect any decent CS program to enable someone to build a useful mental model of what's going on. Plenty of subject matter experts write very valuable code without that knowledge, but they tend to hit a very real wall.
From what I've heard about tuning Haskell code for performance, much of it depends on the particulars of the compiler, rather than on the underlying CPU.
You can for example analyze a program assuming an ideal compiler (which I have seen people do), or you can understand the actual compiler used. The second is an implementation detail subject to change, but it’s also more accurate.
I recall one meeting when people said doing comparisons with a list of objects one comparison at a time should be as fast as doing the same thing one object at a time. I pointed out that due to cache issues doing each check an object at a time would be faster. A few people where shocked when the test showed a significant improvement.
As we don’t yet have such an advanced compiler, impure hacks like `par` start seeping through the cracks.
I have struggled with the concepts of Java for a long time, especially with the many keywords that I cannot relate to, private, final, static, void while I understood majority of Clojure at the first glance. I could not write Java without an IDE but more than happy to develop Clojure with VI. It appears to me that we overcomplicate things for no good reason and underestimate the power of simplicity.
Procedural code is even more central, and should be covered in depth.
I currently program for a living with Java. It clicked with me the moment I first learned it. (It was also my first introduction to OOP.) Right now I’m struggling to learn the nuances of functional programming with both Scala and Haskell. Do I consider functional programming, Scala, or Haskell inferior because they’re not as straightforward for me as Java (or C#, or C, or even ASM) was? Of course not.
And one of them is axioms no-one ever communicates. I've worked with programmers with at least three markedly different axiomatic bases, for want of some less pretentious – and less exaggerated-for-rhetorical-effect – way of putting this:
* `Electrical engineers`. "Computers are imperative because computers are just circuits". Functions, objects, mathematical abstractions in general are fundamentally leaky and to be regarded with deep suspicion. Paradigmatic languages: C, asm.
* `Pure mathematicians`. Computers are abstract machines for manipulating symbols. Programming is set theory; hardware is an implementation detail. State is just an artifact of insufficient precognition. Paradigmatic languages: ML, Haskell.
* `Approximators`. These folk rarely come from computer science backgrounds; instead they tend to come from "technical computing", meaning sciences, engineering, economics, statistics and the like. They're also on the rise, because this is the group of people who "get" machine learning. Computers are fancy and very fast slide rules; their job is to run approximate numerical methods very fast. The only true types are `float` and `bool`; programming is translating linear algebra into algorithms which estimate the correct results stably with bounded error, ideally by calling the right bits of LAPACK. Paradigmatic language: historically, Fortran; these days, whatever array language is embedded in the libraries they're using, surrounded by Python or (if statistician) R.
The point is; these are three markedly different worldviews and none of them are any more fundamentally wrong than the others – they're all useful and wildly incomplete. So unless you can get agreement – or at least empathy – within your team, you're going to spend a lot of time talking past each other.
For a lot of the people I work with code is just a way of representing mathematics. So you end up with "Fortran written in every language"
Here is a snippet of code (this is written in C but I guarantee most of my colleagues would write this the same regardless of it it were fortran, python, Matlab what ever).
for (i=m1;i < m2; i++)
{ //f(p)^2 = (u^T)(Q^T)(D^2)Qu and F(dF/dp) = (u^T)(Q^T)(D^2)Q(du/dp)
g =h;
h = (v[i+1]-v[i])/(x[i+1]-x[i]);
g = h - g - r1[i-1]*r[i-1]-r2[i-2]*r[i-2];
...
}
SELECT t2.Line, t2.Slope, t1.X, t1.Y, t1.Y - (t2.Slope * t1.X) as Intercept /* B = Y -Mx */
OTOH, I would also place myself somewhat in the 'mathematician' category because I see imperative code as functional code where each instruction is a function that takes the current machine state and some parameters and computes a new machine state. The new machine state is an input for the next instruction. When you see it that way, instruction pipelines in the CPU become very easy to comprehend: the CPU calculates one or more possible future machine states while waiting for a response from DRAM, then selects the correct state based on the response.
Seeing it that way also reveals the main issue with imperative programming: the each instruction accepts too many inputs! Functional programming helps constrain the inputs so that it's easier to reason about what the code does and how it can change.
Pretending a computer is somethings else can be a useful abstraction, but you can actually learn what’s going on.
Personally, I've always loved both paradigms, and I've never been able to decide which one I prefer. I tend to move between the 2 depending on which one works better for the task at hand.
That realization (along with the fundamentals required to understand both paradigms) was one of the most useful things I got out of my degree.
No. "Syntatic sugar" implies that it is relatively trivial 1-1 translation that could in principle go backwards. Functional programming has many, many more optimizations and transformations.
Here's a quick overview of how the Actor model is better than shared state (mainly by avoiding locks and nondeterminism): https://doc.akka.io/docs/akka/2.5.3/scala/guide/actors-intro...
And just as an aside, I haven't fully learned Rust yet but from what I understand, the borrow checker only applies to mutable data. If you write a fully immutable Rust program then you can avoid it altogether. So to me, this is a potential bridge between functional and imperative programming. It also might apply to monads, since (from what I understand) languages like ClojureScript can run in one-shot mode where all side effect-free code runs completely and then the Javascript runtime suspends execution, only starting it again once new data is ready. This might also be a bridge between functional and imperative code, because I've found monads to be one of the weakest links in functional programming and I've never quite wrapped my head around how they work or if they're even a good abstraction. Maybe someone can elaborate on them!
In short, the goal here is to reduce all concurrent code to a single thread of execution that is statically analyzable as much as possible. So a typical C++ desktop app may not see much benefit from this, but anyone who has found themselves in Javascript callback hell can certainly appreciate the advantages that async/await provides, since it more closely approximates the message passing of Erlang/Go, which is more similar to shell scripting. If we had a "perfect" language that optimized all code to be concurrent as much as possible, for example by converting for-loops into higher order functions like map and then running them on separate threads behind the scenes, then we could offload the wasted work currently done by humans onto the runtime. So that would mean that instead of writing programs that, say, access remote APIs, cache the data somehow, remember to invalidate it when the source of truth changes, etc etc etc, that complexity instead could be reduced to a dependency graph that works like a spreadsheet and updates all dependencies when something changes. This seems to be where the world is going with reactive programming, with a lot of handwaving and ugly syntax because it's reimplementing old concepts from Lisp etc: https://en.wikipedia.org/wiki/Reactive_programming
Sorry this got a little long, I could ramble about the downsides of programming in these times for hours.
This is not correct. The borrow checker applies to references, both mutable and immutable.
>Sorry this got a little long, I could ramble about the downsides of programming in these times for hours.
Haha, programmer talk is the best!
For a quick breakdown of why CSP and the Actor model are both Good Ideas:
Think about any concurrent system (i.e. multiple threads of execution). Any modification of a shared resource by one thread (one concrete example is a global variable, but filesystem, devices &c. all apply too), is implicit communication that can happen at any point whatsoever in another threads execution.
The state of one thread being modified in unsynchronized ways in another inevitably leads to bugs that are very hard to reason about.
Both CSP and Actors involve removing the implicit communication and replacing it with explicit communication.
Two Unix processes connected by pipes are one example of this, since two processes do not typically share any writable memory.
I don't know if you've written any code designed to be used over a pipe. If you have, you may notice that you do not care at all when the process on the other side of a pipe writes to variables. You do not need locks or mutexes or semaphores or any of those constructs for IPC in this situation.
I don't know if you've ever written any multithreaded code with shared variables, but if you have, you've definitely noticed that you need to carefully hand-synchronize modifications to those variables.
Now of course, the only special thing about the unix processes example was the lack of mutable shared state, and the use of an explicit communication channel. You could write a single-process with many threads that communicate over such channels to avoid the IPC overhead of unix, but still get the simple-to-reason-about concurrency of processes.
Pretty much all of the ideas above was published before 1980.
My dad read Hoare's CSP paper when getting his Masters degree and he told me "80% of the class didn't understand it, and the remaining 20% of the class thought that manual synchronization was not a problem" which explains much of the buggy, highly concurrent software written since.
1: https://en.wikipedia.org/wiki/Communicating_sequential_proce...
>"80% of the class didn't understand it, and the remaining 20% of the class thought that manual synchronization was not a problem"
Unfortunately it seems to be this way with many things in our field (/life?). And the 80% non-understanders group doesn't even stay the same people for every topic! :)
Unix processes work on the opposite side: you can mutate everything, but very little is shared.
With threading and impure code you need to not mutate shared things, and limiting yourself to message-passing is a good way to achieve this (of course you can't message-pass shared pointers or you've missed the point).
Knuth would probably disagree.
I have seen plenty of universities teach Java and C++, haven't seen any that teach actual OOP. James Coplien aptly calls the current paradigm "class oriented programming".
"public static void main()"
In order to understand it, you need to have a good grasp of classes, static methods, access controls.
This is usually followed up by a request to ignore the entire line, which is one of the worst habits you can have as a developer.
Then you have to compile this. It used to be the case that people would copy and paste command line excerpts (bad habit!), but now they will get a pre-configured "IDE" where they can punch the compile button (ok, but I have met plenty of professionals who never left this stage).
Instead, they could avoid the whole thing by using something else, say, Python, or even Javascript. In both cases you can quickly drop to a repl and start trying stuff out.
Once the basics are there, then you can proceed to object orientation. And perhaps even to Java as a more advanced course, only you now have the proper concepts to understand the very first line you are supposed to write.
Why would universities teach Java and C++ anyway? They are either 'boring' from a computer science perspective, or too convoluted for teaching concepts.
Not a fan of Java by any means, but they should teach Java so graduating students can put that on their resume and get a job so they won't live with their parents until they are 35....
It is usually a request to ignore it for now, because "we will get into each part latter". I fail to understand what is so bad about it. It's just not practical to provide all the theoretical foundations upfront, and postpone practice to the second semester.
Up to this day, I still think that the easiest way for me to learn a new language is to copy some hello world, and replace one line after the other once I get why they are there.
I prefer teaching programming with a language that minimizes the boilerplate required to get started.
Static may be hard to understand, but it is something you just can do. You can say(hi) and that requires nothing, but you cannot drive() without a car.
One of the first CS courses at University was OOP in Java. I really struggled to grasp OOP, for most of the first year. It didn't "click" until I tried doing it in Python; after that I went down the rabbit hole into meta-object protocols, Smalltalk/Self/Newspeak, etc.
Java seems to occupy the opposite of a sweet spot: it makes learning difficult for newcomers, yet it's very limited and restrictive for those with experience. Not only is it overly verbose and ceremonious compared to untyped languages like Python, but also compared to ML/Haskell, whilst being less expressive and less safe!
Stop reading here.
(Since Bertrand Meyer, driving force behind the language and course, retired, the course is now taught using Java.)
However it would require a culture shift as a university being a place to get you ready for a career in industry rather than academia.
Because you are prepping for academia it is OK for them to postpone functional to later years on even the PhD.
You mention grief with OO - but I think a lot of it you would get with Functional too and it has more to do with the incentives and people structures in organisations that produce code. Usually praise goes to those who get a 8 hour Jira ticket done in 4, or a 5 week task done in 4 weeks etc, and from the users point of view 'it works'. The structure of the code is not discovered until later.
Code reviewers are working at the deckchairs level, they are unable to change the Titanic's direction, and again both parties in a code review have incentive to do it as quick as possible (while not looking like they obviously brushed over it), so it become mostly a potential bug hunting and syntactic cleanup exercise.
It's almost a running joke that refactoring rarely gets done, and if it does it is trivial, and usually required some stealth from a developer or manager to create cover to do the refactor.
The only hope we have is to work somewhere where there is a good understanding of code quality from top to bottom in the org, or at least when you cross the technical/non-technical boundary there is a high degree of trust to let the tech people do the right thing, and not KPI them into submission.
I'm still in mourning though imagining how far programmers could go if they weren't stuck endlessly debugging imperative code that will never be deterministic or free of side effects. Lots of lost potential there. I'm coming up on 3 decades of experience doing that and it feels like well over 90% of the code I've written was a waste of time. I guess it paid the bills though.
Anyone can learn to program spreadsheets, because spreadsheets realize that state is the most important thing, and puts it front and center—hiding the calculations. Most programming paradigms are about manipulating the calculations, and the state is only visible when the program is running. As long as programming tries to avoid state, it'll be hard for most people to learn.
How can we bring state forward during development?
Most CS curricula have a course where you spend time programming in a variety of different programming languages, in different paradigms.
And that's why I despise code reviews. There's obviously not enough time allocated to them for in-depth understanding of the reviewed code, so I'm mostly spending precious resources (attention, energy) on doing a half-assed review that is not going to do that much good. It feels like such futile work.
This is very true. I hate parsing code written like this, or code written using a mashup of concepts, requiring mind gymnastics to fathom an implementation of a solution to a relatively simple problem. It makes the job so much more unnecessarily difficult.
Points for simplicity if you ask me.
I don't think this is a fault of functional programming as much as it is a fault of implicit language constructs. There are common conventions where being able to chuck functions and closures around is actually useful (e.g. sorting). These language constructs/conventions are useful because they can be extremely expressive, but unfamiliar implicit behaviors cost me much more "working memory" to understand when I'm reading the code.
There's a version of object-oriented programming that mostly sticks to declarative behaviors and uses inheritance, unions, mix-ins, etc. to actually hide behavioral abstractions. The problem is that it often takes 5-10 years of experience before the programmer (myself included) begins to appreciate how important future readability of the code is, and to understand that the more exotic language features should be used sparingly.
They are not in fact equivalent, unless the functional programming you're doing is trivial.
Good luck. Computer Science degrees are balancing act between practical and theoretical. More importantly students want to work with technologies that are popular in the industry today. You can try to to stand against the tide, but you will lose.
Functional Programming will follow the same path. You probably don't like it for it will be ended up impure and just some syntax sugar that looks like FP, but rest of the world like it because it gets the job done.
Wrong.
> So practical languages took the good idea out of OOP for convenient syntax sugars.
Also wrong, unless by "syntactic sugars" you mean "nontrivial compiler rewrites"
> Functional Programming will follow the same path.
Doubt it.
> You probably don't like it for it will be ended up impure
Purity does not constrain efficiency at all.
At an abstraction level below digital circuits, you are correct. But thankfully the layers on top of that do almost always do a very good job of hiding it.
>Doubt it.
Functional programming is already following the same path. Sure there will non-hybrid languages around if you want to use them, but take a look at the functional constructs that have made their way into almost every procedural language in use today.
Most people have never touched Haskell, but almost everyone has seen a map function.
>Purity does not constrain efficiency at all.
Maybe not inherently, but there's a reason we have to break out and use mutable data structures when we really need performance. For the systems we are working on today purity does impact performance/efficiency.
https://en.wikipedia.org/wiki/HyperCard
http://mstay.com/images/screens/vpc1.gif
So thought of code as a big flowchart where you fill in the boxes with business logic. Transitioned to C within a year or two and got incredibly deep into assembly language and low level code for blitters back in the 486 era when DOOM came out. Unfortunately moderately priced Macs were an order of magnitude too slow to play fullscreen scrolling games at 640x480x8 resolution until the 60 MHz PowerPC came out in the mid 90s. So never made any real money on Mac shareware games, but I digress.
The Mac had an informal programming environment (no console or office suite with standardized inter-application communication) and I hadn't seen MS Access or FileMaker yet, or spreadsheets. When I first encountered them for writing reports in college and it finally clicked for me that code didn't have to be run imperatively, it was devastating in a way. But I made a full recovery in the early 2000s when PHP/MySQL got popular and I was able to get back into rapid application development with ORMs. I feel like the world is about ready to make the jump from hands-on tools like Laravel to WYSIWYG tools like Wix. Most of the attempts I've tried are frankly terrible, but I'm optimistic.
Here is a straight up comparison someone made if anyone is interested:
The quote at the end sums it up nicely. Coding should be the easy part. A sentiment everyone tends to nod their head along with, but rarely has the discipline and willpower to implement.
I see writing software to be similar to writing music. Music has rules and structure, but leaves room for creativity and allows two or more highly skilled musicians to be able to play music together and improvise.
Static typing imposes limitations (kind of like government), whereas dynamic typing gives you more freedom (but requires responsibility)
Design your product with as much free thought and creativity as you please, but never let yourself believe your actual code is art. That - among many other outcomes - is how your platform gets compromised and your customers' identities stolen - not to mention how the successors to your job end up cursing your name and wasting time and money replacing your code wholesale.
Or, imagine dropping all regulations around planes, cars, food, health care or infrastructure. Would things be handled better by artists, free to pursue quality? Maybe. Will majority of the providers be artists, or even care about quality? No.
If anyone has any survey or any discussion on that please reply so I can take a look at it. I'd like to confront my expectations with data
Bad music carries only the risk of people not liking it. Bad code on the other hand...
Rarely does it kill and in those cases (self driving cars, banking) those application usually has a company behind them.
Static typing helps to minimize bugs (when used correctly) by allowing function contract declarations and reducing the build up of defensive guards over time. I've seen code in dynamically typed languages with lines like `if (!foo is integer) raise;` which basically equate to onerous home-built static typing.
Why would guarantee free software have no value. It's like buying a used phone.. no guarantee but it still has value.
<braindump>
I agree that coding/development is an art, but I also am hard pressed to find anything that, when done well, isn't an art.
The difference is that music doesn't have any really notion of correctness or efficiency; sure, there are ideas such as "no parallel fifths" and "tritones must resolve to M3 or m6", but this isn't an issue of correctness, but rather stylistic guidelines. Schoenberg's compositions weren't incorrect in any universal sense.
Programs, on the other hand, can be incorrect or inefficient. This is because most programs have a concrete function that they produce.
Dynamic types are great for exploring your solution space. I can quickly whip together a prototype, try out different solutions, etc. I don't need to design my entire program ahead of time, and this is nice. However this does not prevent me from reasoning formally about my program. Once I've muddled around a bit and built up some scaffolding, it very well may behoove me to try to shore up my design, spend some time reasoning and designing a formal algorithm/specification/etc, etc.
And for the record, as a musician I definitely think formally about my compositions/pieces I'm playing. Granted, being a guitarist this usually doesn't involve me writing out my pieces with sheet music, but there is still a blend of intuition/exploration and brute computation.
As an example, I often times have two disparate parts that I need to connect together, maybe by modulating, maybe by changing registers, or maybe by altering my time signature. At that point I put the guitar aside for a moment and think about my formal requirements, and then try to find some 'convincing' way to get from point A to point B. Maybe I have some constraints (I have two measures, I need to start in this position and end in that position, this finger needs to pedal this note, etc). This quickly becomes a math problem where only a small set of viable solutions exist. After 'doing the math' I am left to evaluate my solutions aesthetic quality which, I suppose, is where most people think of the 'artistic' bit comes into play. But really, I'd say artistry abounds throughout the process.
And to be clear, I'm not thinking about this stuff as doing math as I'm doing it--I have my own system for thinking about this stuff that doesn't look like math.
Anyway, all of this is to say that formalism can be used even in music with very real benefits.
</brain-dump>
This is because given all of the levels of various languages, frameworks, and libraries- I'm just trying to get things to work.
However, I would very much like the methodical engineering approach at my day job applied to programming.
It really blows my mind we don't have full stack + auth that works cross platform out-of-the-box. It blows my mind my recent framework didnt show the post request exchange to get tokens and authenticate.
There are NOT that many people that program at this level. It seems most of my programming questions are answered by asking experts rather than reading a wikipedia article. Electrical and Mechanical Engineering are better solved reading rather than asking engineers. IMO.
where to begin
Critical-systems software engineering is not about your creativity, it's about building maximally correct software, to minimise the probability of a catastrophic outcome.
This idea that it's inherently virtuous to let software developers be creative, strikes me as quite wrong-headed. If a strict methodology produces better results (and it does), a strict methodology should be adopted.
Bridge engineers don't whine about their constrained creativity. They're too busy ensuring their creations don't get anyone killed.
With the curious exception of Erlang et al, few people serious about program correctness favour dynamically typed languages. There's a reason why Ada is statically typed, and strongly typed (it lacks the dangerous implicit type conversions permitted by C).
An excellent article on this kind of thing: https://www.fastcompany.com/28121/they-write-right-stuff
Them, "All that extra effort sounds great, but we don't have the time to do that. It will explode the really tight build, test, debug cycle we have now. Suddenly every cycle will be 100x as long."
Me, "First of all, you should be less concerned about the length of an individual cycle and more concerned about the sum of all the cycles up to completion."
Them, "Okay, but having short cycles also helps us course correct quickly, and keeps our 'velocity' up."
Me, "Well, second of all, what good is it to be able to iterate really quickly toward an unspecified goal? How do you know that what you're doing will get you there? Or worse, how do you know that what you're trying to do is even possible or not? Maybe you're 'engineering' your way asymptotically toward an impossibilty result."
It's sometimes crazy making to have these conversations and see how wildly distorted we've allowed our incentives and perceptions become as a group of professionals. It's become more important to produce the appearance of progress and effort than it is to actually make progress and thoughtfully apply effort.
I would also caution you. Do you really know the technology that you are trying to make safe? Building systems with research / deep learning is as different from traditional software development as synthetic biology from electrical engineering.
Yes, it's true that most companies hire way more people, way too quickly than is probably prudent for a problem domain (especially one that is still such an open-ended science project like AVs), and that as a result barely anybody has any idea what they're doing measured against what's being expected of them, but that's a wound that is entirely self-inflicted. It's not a natural law that one needs to suddenly staff up dozens or hundreds of really expensive people ahead of any real capacity to train or assimilate them, but it does happen with depressing regularity. If anything, I'd say this is probably the biggest problem I see in the ecosystem that you and I are in.
The team I work with is small. Everyone has several (5-15) years of experience consuming research, turning it into practical solutions, and in some cases even having created a novel practical application that was later supported by adjacent research.
It's not easy to construct a team of half-dozen to a dozen prolific programmers w/ a bent toward the academic, but an innate sensibility for remaining pragmatic and applicable. But, it's also not impossible to do so either. This is inline with my incentives comments elsewhere. I think the incentives are broken at too many layers to be able to be fastidious and intentional about how we solve problems. Say you get an "empire builder" into the leadership structure... you're doomed. The whole point of everything becomes about having as big of a "rockstar" team as possible, not about trying to solve a problem. Unless the problem one is trying to solve is how to quickly become the SVP of an extremely expensive and probably fairly unproductive team of increasingly disaffected previously very effective people.
That said, you'd be right. Not 15-years in something like computer vision. No such thing as formally verified NNs, regardless of what nuTonomy claims, exist. Even the basis about what one would be trying to verify is an open question. It's partially the point of DARPA's Assured Autonomy program.
The problem at the moment is that the ecosystem has two science projects on its hands. How to make an ML-derived driver is one. How to make a stable, correct substrate for acquiring data, make a decision, and react correctly is another. The only one most people hire up for is the former, and the latter is at least as challenging.
There's a layer of it (the AI/ML bits) which is necessarily probabilistic. That's by design. It's how it all works. All the layers below that today are currently terrifyingly probabilistic. It's difficult to advance the capability of the whole domain when the necessarily probabilistic parts are depending on shifting sands as a stable foundation.
I agree though that there's a large gap there in the domain expertise of the parties involved, and that's produced significant challenges as we've not yet figured out how to close that gap.
Though, I'm happy to be proven wrong here as it would make me a lot less nervous about the future were there a way to legitimately assure the artificial driver in an AV won't fail in emergent ways, or at all.
LUCRETIUS, De Rerum Natura
:)
I like to think of it in terms of quantifiers: for most systems it's fine to say that there exists a set of representative tests that the system passes. For critical systems, you really want "for all" in there instead.
Fortunately the model-based systems are much easier to reason about, even if they suffer from difficulty modeling certain cases. For a model-free system I think the starting point would be to precisely state a correctness criterion that could be used as a decision procedure on the output of the model; the combined system would be "verified" to a certain degree. Unfortunately you can't guarantee that it would always be able to yield an answer (it might always give a bad one which was rejected) and, the more fundamental problem, one might reasonably expect that if you can express the correctness property to a sufficient level of detail that you can perform verification on it you might be able to write an easier-to-verify implementation that doesn't rely on ML.
This stuff is hard, yo.
1. What parts of AI/ML have to be nondeterministic?
Once the model is trained then it should be completely deterministic. There are some training techniques that randomize the order or grouping of data, but they are primarily used because random is almost as good as finding the optimal ordering/grouping and finding the optimal ordering/grouping is hard. Sometimes randomness is used to augment the data to give you more examples to for against (because the model is too complex to train/fit with the data you have it you want to be robust to certain variations in input. If you're talking outputs then you should get the same outputs from a model given the same inputs. There are some really bad models out there that are way over fitted (relevant xkcd - https://m.xkcd.com/2048/ see "house of cards") and some people working on ML have a terrible grasp of statical techniques (just try models until they find one that fits), but even these models are deterministic.
What is so bad about nondeterminism anyway? Ethernet used nondeterminism to handle collision resolution. There best prime finding algorithms are nondeterministic. There is nothing wrong with appropriate nondeterminism.
It can't possibly be more efficient to take 50 fairly expensive people and have them iterate 10,000 times toward something that still ends up being fairly broken---and requires maintenance in perpetuity---than it is to take 6 slightly more expensive people, and have them iterate 10 times toward something that does exactly and only what it is supposed to do and requires basically no attention once it's been instantiated, can it? Even if you're Instagram.
That's why I'm sceptical about going to work on the autonomous vehicles tech (although it is tempting). I'm affraid there's been so much money and hype around it that "failure is not an option" - i.e. companies will sooner see another Challenger disaster than admit that they're not on track for their announced goals.
Commercially speaking - it's usually not.
To me it seems like an incentive problem that starts with the distorting effects of unsophisticated investors w/ unrealisitic expectations who fund following a herd mentality only things they can themselves pattern-match to.
> To me it seems like an incentive problem
Why is it a problem if a buyer gets something that works well enough for a lot less time/money put in?
Further to that - specifications and requirements are often imperfect, poorly pinned down, ever-changing. Software creation out in the commercial world has shifted working patterns to try to adapt to that (Agile methods amongst others). Attempting formal proof of such soft, malleable systems would appear to be a fool's errand.
The challenge with this formulation of "ever-changing" is that it assumes that things like Agile methods are somehow creating the capacity to iterate toward something of value with intention and ambition in such a way that you'll achieve whatever it is that you're trying to achieve.
However, what happens is that the lack of rigor in software development today seems to cause the lineage of development and associated created technology to drift further and further away from the desired commercial goal as those goals change or mutate.
Creating a bunch of brittle technology and technical debt to poorly approximate Purpose-A (a purpose by the way that you might be able to formally prove trivially is actually impossible and you either shouldn't waste the money or should intentionally select the best sub-optimal solution) doesn't help you get to Purpose-B any faster. As you become aware that Purpose-B is a thing you need to angle toward, you're still dealing with the pile of bubblegum, toothpicks, and instruction manuals written in alien script that still hasn't achieved Purpose-A.
It's a really weird thing to me that as an entire ecosystem and community we've decided that the most valuable way to approach software is to declare that it's impossible to ever "finish" it.
If I have a series of high-assurance layers to build upon that I know I can trust, then iterating and adapting to changes actually becomes faster and easier, because I know the surface area of where a problem can actually reside and how deep in any part of a system I actually have to uproot and start over. In the current formulation of the world, basically everything is a suspect, and basically any solution is considered viable... whether it truly is or not.
I've been in situations where Product Managers and Engineers spent months off and on arguing over some proposed solution or feature and never getting anywhere because everybody's basis was built on social capital, political capital, and mythology. What finally killed the conversation and allowed progress to actually happen? When a TLA+ model that invalidated one of the proposed hypotheses was presented. "Well, look. The way you want to do this is actually impossible. It will need to be done like this, this, or this instead." Seven... _seven_... sprints of about a dozen people wasted because nobody could formalize either the requirement or the approach. Until somebody did. This wasn't for a safety-critical system either.
If you're doing it reasonably well, they produce small chunks of something valuable every iteration.
> Creating a bunch of brittle technology and technical debt
Who's creating brittle software or technical debt? Things can be well designed and well written, well structured and well tested without going as far as formal proof, which in most commercial situations is going to be masses of overhead and quickly not applicable to the ever-shifting problem domain.
> It's a really weird thing to me that as an entire ecosystem and community we've decided that the most valuable way to approach software is to declare that it's impossible to ever "finish" it.
You seriously need to get out into the commercial world more. Or perhaps into the smaller, faster moving commercial world (I'm not sure where you are now).
> If I have a series of high-assurance layers to build upon that I know I can trust,
Then the underlying assumptions are likely to change, rendering your layers an expensive boondoggle.
> I've been in situations where Product Managers and Engineers spent months off and on arguing over some proposed solution
Then you have bigger problems than formal proof.
I'm generally looking at things which are designed and delivered within a number of months - anything that takes months to argue over has entirely missed the boat as far as I'm concerned.
A business process that works "by itself" most of the time, but requires human intervention once in a while, is still a functional business process. The unit of "software + 5% of this person's time" is perfectly workable. And if the cost of the fix is more than the NPV of 5% of that person's time, it isn't worth making.
Catastrophic failure risk, of course, changes the analysis. But a huge range of things are not catastrophic in their failure modes.
I don't know. Maybe I'm jaded, but I think in B2B, good software is not even desired. In B2C, sure, as Apple proves, but not in B2B.
You can make good software without formal proofs. It just may not be proven to be perfect.
> They want to be involved in the process. Make dumb decisions.
This I agree with though, sure. They do make dumb decisions, and they push ahead anyway, even when told. Later they change their minds, we change the software. It's the grand circle of life or something.
Regarding the topic, I think there are multiple ways of expressing ideas, where math happens to be just one of them. For instance, for the Greatest Common Divisor example, you could just say that "if x equals y the cgd of x and y is x, else you need to keep subtracting the smallest number from the largest until both are equal".
You could use simple math, such as:
/ x if x=y
gcd(x,y) = | gcd(x-y, y) if x > y
\ gcd(x, y-x) if x < y
def gcd(x,y):
if x==y:
return x
elif x>y:
return gcd(x-y, y)
else:
return gcd(x, y-x)
In the end, I got the feeling that he is trying to "sell" us his TLA+ approach.
gcd x y | x == y = x
| x > y = gcd (x - y) y
| otherwise = gcd x (y - x)
I hope TLA+ gains more popularity. It's an interesting technology.
https://hitsmediaweb.h-its.org/Mediasite/Play/abdee6c8696a48...
The desire for reuse is not driven by a want to reduce LOC, but hours spent.
I guess there are occasionally pieces that could be used as-is (e.g. a description of a lossy network), but those tend to be so simple, that looking for them in some Maven-central for spec modules would probably more effort than writing them from scratch every time.
So yeah... you end up with a beautiful mathematical expression ... but runs way slower than an "ugly" equivalent in c code.
The goal should be somewhere between the two levels. Most code doesn't need to be as efficient as hand-tuned assembly. And most languages aren't so bad that they create many orders of magnitude difference between that hand-tuned assembly and themselves in performance. C may keep you within the same order of magnitude as that hand-tuned assembly. But ocaml can as well, and offers much cleaner expressions of many algorithms and ideas (closer to their specification concept than their machine code run time).
When one language becomes insufficient, accept polyglots. If Erlang's mathematical computations are too slow, create a C program that can be loaded in, or that calls out to OpenCL if need be. But Erlang's ability to express concurrency is among the best, and C's is among the worst. So why use one of the worst languages for concurrency when you can use one of the best, and restrict yourself to C code where needed?
The same consideration should be applied to other problem areas. Logic languages and constraint programming can solve many computational problems, and often very efficiently. But both are light years away from the underlying machine they're running on. Should they be discarded so we can hand write and hand tune a constraint solver in C every time?
While it's wasteful to rewrite everything 10 levels above your hardware (an interpreted language, running on a vm, running on a vm, until eventually you find the CPU), it's hardly appropriate to drop everything and insist on the lowest level (or near lowest level) language around. Instead, drop those inefficient languages that barely add anything of value (no novel capabilities, no better safety guarantees), keep the ones that are reasonably efficient or maybe inefficient but offer some true utility. Then code in the highest level language that's reasonable, moving down the stack only when needed for performance (or other) reasons.
Portability comes with a price. And the more you abstract away from hardware the less you will be able to use it to its full potential. Most of the code written in these times it's not designed around things like cache locality for example and we have code that is 100 times as slow as they should be... even in plain C!
That said, we can agree that right now (more or less) you can reason about cache locality (for example) in "traditional" languages (even in Javascript... to some extent) and keep your distance from bare metal. But you lose the ability to reason about that and other things by using a PL so focused in writing beautiful mathematical expressions. For me, that's a deal breaker.
Understanding your hardware is only half the story. To use the hardware effectively, you also need to have mathemaitcal insights into your problem.
A rather extreme proof of this fact is bubble_sort.c vs. quick_sort.java. I think it's clear which of those is using the machine more effectively...
> I doubt you can achieve great performance on a language that focuses entirely on mathematical representations without considering the hardware.
Plenty of very high level languages have extremely effective compilers. SQL query engines come to mind.
> So yeah... you end up with a beautiful mathematical expression ... but runs way slower than an "ugly" equivalent in c code.
TLA+ et al. are about primarily about correctness and designed for situations where correctness is hard to get. Beauty is relevant only in-so-far as it helps one the path to correctness.
But yes, hand-craft code will get you your GIGO much faster :)
There's nothing special about the cache hierarchy. It's just one more thing that can be reasoned about using mathematics. If you care about cache locality, you can write down the semantics of an optimizing compiler and prove that this compiler uses the cache hierarchy in an optimal way. Why would that be impossible?
Not only is it possible, but it might even be easier in high-level languages. For example, the argument has even been made that the importance of cache locality is really an argument in favor of higher-level functional languages.
But again, with respect to TLA+, this is all a red herring and completely misses the point. The more important point re: TLA+ is the GIGO/correctness problem. I don't give a damn how cache-efficient my algorithm is if it's not even computing the correct results!
There is a huge, dark-matter body of software development that goes on in the world under the thumb of megalomaniacs whose only metric of productivity is how much unpaid overtime his programmers are working.
Edit: Never mind. I found the slides he had made for the same talk given elsewhere. https://drive.google.com/open?id=1sZciK13LDh4rBFwbRCk0Oylga3...
- Why is this the case? Even if it's true, it hardly seems obviously true.
Now, machine learning to find bugs or adjust variables... yeah. I can see that.
In Automator, pre-made blocks of code that do different things (filesystem manipulation, data transformations, application control, machine control) can be assembled into a workflow, and configured with options. It is possible that something like that could be given a speech-based UI (rather than keyboard and mouse) and the result is that pre-existing code is assembled and configured. That's a lot more realistic.
For example if I remove a global variable from a source file and another branch adds another reference to it, if it does not occur on the same line git will happily merge the file with no conflict.
On the contrary, I think machine learning might be more immediately useful for things like low-level optimization.
Here's a thought: PL researchers seem to generally agree that typed languages are superior to untyped languages, yet programmers tend to prefer untyped languages to typed languages, to the point where Java and C++ have the fanciest type systems in common use, with ML being the closest thing to an academic language that gets significant use.
It seems intuitive to me that typed languages are bad for exploring algorithmic design, so could this where the disconnect is? Most programmers do not know what algorithm their final product is going to have when they start and dynamic languages are much more ergonomic when you are exploring he design space.
Certainly if I knew exactly what program I was going to write when I started, I could probably write it in haskell; indeed once I have a working program, translating it to haskell is often fairly mechanical. However much of my time is spent trialing algorithms that may or may not be a good fit for the problem I'm solving and in those cases I feel like haskell gets in my way, while lisp gets out of my way.
I don't know if there is any practical takeaway from this, but it does seem to at least give an explanation for the divide between PL theory and practice.
I have not found this in practice. I have found that some developers prefer a dynamically typed language for certain situations, like rapid prototyping. However when maintaining code bases, I've found that developers often bemoan the lack of static types to assist in small modifications to code they haven't touched in a while.
Personally I love the ability of static, declared types to organize assumptions about code; I also love the ability to do terrible things to types to shoehorn poorly designed third party libraries into my codebase. I don't see it as a developer preference so much as dependent on the problem domain.
If I could have a dynamic language, and static typing, that would be the best of both worlds. However, gradual typing doesn't seem to have caught on.
I don't find myself actually using gradual typing though. Not very often at least. Even in prototypical stages of an application, I usually just put together the types of what I currently have, even if I think they will change later.
I have found it very useful for things like translating incoming JSON or XML to the typed world. As long as the input data is of known format dynamic code is much shorter and concise.
To give a concrete example, suppose that you have a weighted graph whose weights are integers. Code to find a Minimum Spanning Tree will always have an integer for the weight. Great. But if you add that type annotation, you'll run into trouble when someone checks whether the previously found MST is unique by calling the same algorithm again using as weights (weight, edges_in_common_with_prev_mst). (This will find the MST that shares as few edges as possible with the original, so if there are > 1 you'll find a different one.) Those ordered pairs were just fine in the original code, but don't fit the type annotation.
Of course, you want to use data correctly. There was a study of server code in Python that found that lots of playing fast and loose with type information happens just after startup, but then types settle down. If the initialization can be isolated in certain parts of the code base, it would make such date easier to use.
I recently tried to port an ~11k SLOC object-oriented Perl program from GTK2 to GTK3. The lack of types was maddening. I would have some simple goal, like "find the path of $image." I would immediately run into a roadblock: what type is $image? Is it a string? A file handle? A Gnome2::File?
So I trace the variable back. It's a parameter, so look at one of the places that calls it. That callsite uses a global variable. Aha! I go to where it's initialized. It's initially set to undef. Dead end.
I couldn't help but think, "I wish I was programming in Java right now." That was a new low for me.
A lot of the new people use dynamic types because that's all they know.
A big reason for the recent shift towards dynamic languages, in my opinion, is what's taught in college now a days. I believe it's mostly Python or the likes. In my college days (late 1990s) it was all statically typed languages (Fortran, Cobol, C, Pascal etc.,). So that's how my generation ended up learning to model a problem and solution in statically typed languages and natural preference towards them.
That said, I find maintaining an old, large application written in an untyped language pretty miserable.
Maybe programming just sucks.
EDIT: Heh, kind of ironic really. A pronoun without an antecedent is like a variable in a dynamic programming language whose context isn't clear.
Maybe a bit less python and a bit more of one of: perl/awk/apl/smalltalk but still they seem to choose untyped languages over typed languages when they are unconstrained to pick the language.
Haskell has ST for mutable local variables, and for the truly "quick and dirty" cases there's always unsafePerformIO. What is it you're trying to express that wouldn't be handled by either of these options?
I don't think that's "getting in your way" so much as asking you learn pure, immutable data structures. Which is good even aside concerns of laziness.
* Distinction between dynamically typed and statistically typed is clear.
* Weak versus strong typing has less clear definition. Usually weakly typed means many implicit conversions between data types and representation.
Most programmers like the late binding approach. That is easy to do with dynamic typing. Adding static typing or type inference for late binding is more difficult.
Programmers usually hate the "weak" typing aspects of their dynamically typed languages when they are chosen wrong. JavaScript is good example of choosing implicit type conversions in a way that leads to confusion.
Not so clear as you might think. For example, it's relatively easy to construct a typed version of the untyped lambda calculus using isorecursive types.
It's hard for actual programmer make that mistake.
The more strongly typed a language is the more it forces you to think about the big picture and architecture your entire application in a way that will map nicely to the type system. For instance with a language like Rust which is both strongly typed and integrates concepts like lifetimes into the type system you need to think long and hard early on about how your "data" and your "processes" are going to interact to figure out a way to map everything cleanly.
Doing this correctly requires a lot of experience. You need to be able to project quite accurately what your project is going to look like (lest you end up to refactoring everything a few weeks from now or worse, lose a lot of time fighting the type system instead of leaning onto it) and you need a deep understanding of your tools to figure out what's the best way to model it and the tradeoffs involved.
If you're a beginner it can be seen as overwhelming and maybe even counter-productive, let me code and stop bothering me about integer to string conversions!
At this point I'm tempted to draw the conclusion that "dynamic languages are for n00bs and static typing is for the 31337" but my self-awareness douche alarm is starting to beep very hard so I'm going to deviate and concede that many brilliant programmers seem to favor dynamic languages so clearly some strive in this environment. So instead I'm going to draw a weaker conclusion: while competent programmers may or may not prefer dynamic languages, beginners will almost certainly favor the more forgiving nature of dynamically typed languages. That biases towards dynamic languages in the general population (and especially the population who cares about engaging in language wars in the first place. Us experienced coders know that the only worthwhile debate is tabs vs. spaces. It's spaces by the way).
This is a good point. A straightforward corollary is that the size of the picture can be drastically different for beginners and experts.
One would imagine that beginners work on more small toy projects than experts. In such cases the protections that static languages offer can seem less valuable, and the friction more painful.
It really isn't about competence. Competent programmers can fall into either camp. However there is a strong tendency for people to conclude that people who disagree with them are incompetent. As you just did. And then backed up to realize that there are good people who disagree with you.
I would also disagree with your weaker conclusion. In general bad programmers agree with whatever role-model they have most recently imprinted on. If they've picked up a Java book that talks about typing, they assume that it is right and types are worthwhile. If they pick up a PHP book, then vice versa. The current popularity of Javascript and Python mean that a lot are going to be on the dynamic side, but far from all.
If you have a lot of types of data to model(layers of records, sequences, indirection, etc), dynamic types make it easy to start bodging something together, but result in write-only code. So you end up wanting to have additional structure and definition - maybe not immediately, but just after prototyping is done and you have a first working example.
If you're just applying a routine algorithm that ultimately does a round trip from SQL, you don't need that additional assurance. The database is already doing the important part of the work.
If you have simple data but it needs to go as fast as possible, you end up wanting to work at a low level, and then the machine size of the data becomes important - so you end up with a static types bias.
[1]: Due to the requirement that they be efficiently compiled/interpreted.
With the exception of JavaScript, I only use dynamic languages for throw away scripts.
I had lots of fun with Lisp and Smalltalk, but can't imagine using them with the team sizes I usually work with.
I have an impression that it correlates less with team size, but rather with average member skills.
Well-written and logically organized Lisp code shouldn't be any harder to maintain just because the team size has increased. Rather, Lisp provides too much power (as in, macro system, compiler easily available at runtime, etc). These can be easily abused and wreck a codebase.
I have chosen Golang for most new development in the group I am in, basically because it forces a straightjacket onto people, even down to things like code formatting. I got tired of asking for people to write unit tests for their Python code – the fact that people can get away with throwing Python code with zero tests into production baffles me, it's like taking C code to production without compiling it.
So at least I got a compiler enforcing some level of code correctness and some uniformity in code conventions. And the fact that noone is overriding anything they should not...
So for me, the divide is that the tools shouldn't make me do work that they can do themselves, namely type inference. And I'm baffled that Java people just outright decided they don't want type inference. They chose to type things that the computer can calculate for them! It makes no sense.
Granted, the usefulness of the work I still choose to do scales with the longevity and involvedness of the code, so I dump hints in scripts that will live for half an hour.
That being said the only thing I've run on jre10 so far has been Scala, so ymmv.
If you don't know what program you want from the start, it's yet another reason to write in Haskell.
Haskell programs are much easier to change than any dynamically type language. Each time you change your mind in Python, you have to basically rewrite your entire program, and if done often enough (what 2 or 3 times are already enough) you will still get a mess on the end because of all the changes.
The real problem with all those discussions about types (and why I think nobody should try to pass an opinion unless they tried something at least as good as Haskell) is that the most used static languages have the least constraining, most ceremonious and least expressive systems around. Developers gain nearly nothing from their type systems, but they are incredibly demanding of upkeep.
My larger point is that he seems to be using "programming language" as a shorthand for an imperative, typed programming language. A lot of what he says doesn't seem to apply very well to SQL or Prolog or Lisp, for instance. (I say this having only skimmed the slides, I don't have two hours for this right now.) I won't say that it's a straw man, because there are plenty of programming languages that fit the way he's using the term and some of them are incredibly popular, but it seems to be a definition that leaves out a lot of programming languages.
It is (generally) a requirement that if you're writing a linear time algorithm, then the compiled/interpreted language will be executed in linear time. This is not the case for TLA+. You can describe linear time algorithms in a way that can only be compiled into, say, an exponential-time program, and possibly even not at all (i.e., extracting an implementation is undecidable).
I wrote about this at some length here: https://pron.github.io/posts/tlaplus_part3
> My larger point is that he seems to be using "programming language" as a shorthand for an imperative, typed programming language
He means a language with the property I mentioned above. It is somewhat true that Prolog has a tiny portion of the expressive power that comes from a truly nondeterministic language such as TLA+, but it still falls under "programming language." If you want to get technical, a language such as Prolog can let you program with some limited use of quantifiers. In TLA+, you can specify using unlimited use of quantifiers ranging over infinite and even uncountable domains.
In TLA+ you can describe the property "decides halting in linear time," and then show that a specific implementation can do so in some special cases for example. No programming language can do that (i.e. describe non-computable "algorithms") but it is essential for specification languages.
Coq certainly can describe properties like this; they're just uninhabited types (all the necessary concepts needed to define "decides halting in linear time" can be defined over an inductive definition of the step function for the programming language of the halting decider; or if what you in fact meant was "a type that represents programs that halt in linear time", it's even easier and requires the same concepts, but a less powerful programming language). There is no specification sublanguage required. I find your distinction to be pretty iffy. Of course, Coq is not a very traditional programming language, but it is a programming language nonetheless.
(I note that you claim that Coq separates types and terms into two different semantic and syntactic categories, which isn't really true. The set model, which is the standard model that justifies the consistency of the calculus of inductive constructions, makes no such distinction!).
(To be clear, I do agree that there is a difference between specifying a type and synthesizing an inhabitant for that type; I just think that the "programming-specification" distinction you are making is somewhat artificial, with dependently typed languages demonstrating this particularly effectively by letting you program within your specification as well).
I don't think this is true for Coq. Ultimately, Coq relies on a type/inhabitant separation. When you spoke of Coq as a programming language, the terms you can always "run" are only the inhabitants.
> So it is extremely unclear to me that the distinction you are making is fundamental.
I don't know if it is entirely binary, but it is sufficiently precise for useful terminology. A programming language is a language that can be used for programming, namely it is a language whose every term can be mechanically interpreted in an "efficient manner."
> dependently typed languages demonstrating this particularly effectively by letting you program within your specification as well
I don't think that any existing dependently typed languages do anything particularly effectively (neither programming nor specification), but that is beside the point :) It is certainly possible to combine a specification language and a programming language, but not without some formal delineation or the experience would be frustrating (i.e., it is possible to interpret some subset of TLA+ terms, but I am not sure it can be syntactically easy to determine which). This is, however, something that TLA+ tries hard to avoid as a design principle, because we do not yet know of any feasible way to scale specification from the "program level" to arbitrary levels of interest. Unlike Coq, TLA+ was designed not as a research tool for logicians, but as an industrial-strength tool for practitioners (I wrote about the design principles behind TLA+ in part 1 of my series: https://pron.github.io/tlaplus).
Firstly, yes, it is absolutely true for Coq (or at least, a large subset of it). The set model is essentially the entire basis for CiC's claim to consistency. I'm fairly sure TLA+ also has such a model (somewhere).
Secondly, all terms in Coq, including types and universes, are inhabitants of some type, so there is no distinction between "the inhabitants" and all Coq terms (it's true that weak head reduction leaves products and other obvious types alone, but that's not the case for stronger forms of reduction like strong normalization, or for full conversion). Moreover, the conversion that occurs in the static phase (typechecking) has the same semantics as the execution during the dynamic phase (runtime). So I really don't understand what you're driving at.
> I don't know if it is entirely binary, but it is sufficiently precise for useful terminology. A programming language is a language that can be used for programming, namely it is a language whose every term can be mechanically interpreted in an "efficient manner."
"Efficient manner" is pretty vague. I suspect there are widely used programming languages that will differ by 3 or 4 orders of magnitude while evaluating semantically identical expressions, while nonetheless both clearly being programming languages. Besides, many optimizations are only optimizations for certain data distributions, and if the compiler guesses wrong it can hurt performance; but that doesn't seem to me to have anything to do with whether something is a programming language or not. If all you care about is the default reduction, Coq's certainly tries to be fairly efficient: beyond optimizing the usual lazy reduction, it exposes many other reduction strategies, tuning knobs to tweak how reduction runs to improve performance when domain information is available, and even contains multiple implementations of some reduction strategies so people can select the appropriate one for their use case.
> I don't think that any existing dependently typed languages do anything particularly effectively (neither programming nor specification), but that is beside the point :)
I'm well aware of your biases here. Regardless of their origins in PL research, plenty of useful work has been done in dependently typed languages, including much larger developments than any I'm aware of in TLA+. I'm not really interested in arguing their relative merits--clearly, both are useful--I'm just asking you not to pretend to make general statements about programming languages while actually talking about TLA+.
I am not saying that types do not have a set model, but that types and inhabitants are fundamentally separate. Or, put another way, a lambda term specifies a single (parameterized) execution (up to evaluation strategy), and that is the only thing that can be made to "run" (I'm sure there are ways to extract, say, a sole inhabitant of a type, but types cannot in general be turned into executable programs).
> "Efficient manner" is pretty vague. I suspect there are widely used programming languages that will differ by 3 or 4 orders of magnitude while evaluating semantically identical expressions, while nonetheless both clearly being programming languages.
I'm talking about exponential differences in time complexity, or even infinite ones. You can easily specify "computations" with infinite (or even uncountable) nondeterminism in TLA.
> I'm just asking you not to pretend to make general statements about programming languages while actually talking about TLA+.
My (and I think, Lamport's point) is that there is a fundamental difference between a specification language and a programming language. It is certainly possible to mesh the two and call the result "one language", but then it must necessarily contain two deductive systems, and so I think the distinction can still be made. Even if you object to this distinction, you would agree that the "specification parts" of Coq (i.e. those with significant nondeterminism and use of quantifiers) cannot be generally mechanically executed in an efficient manner. So whether it's two languages or one, there is a fundamental difference between those expressions that can be used for programming (little nondeterminism/use of quantifiers) and those that are necessary for specification (unrestricted nondeterminism/quantifiers).
SQL joins are worst-case exponential in the number of relations joined, where n = the total number of rows in the database (though there are many special cases that can help reduce this). I believe many people nonetheless consider SQL a programming language--with WITH RECURSIVE, it is Turing-complete. You could probably talk me into believing it's more of a "specification language," but despite that people use it for performance-critical things (admittedly usually in one of the special cases where it's better-than-exponential, but such special cases exist for most intractable problems; it doesn't seem to me that the nature of the language can be thought to fundamentally change depending on the data set).
> Even if you object to this distinction, you would agree that the "specification parts" of Coq (i.e. those with significant nondeterminism and use of quantifiers) cannot be generally mechanically executed in an efficient manner.
I specifically object to this! Coq executes what you term the specification parts in a very different way than trying to exhaustively enumerate solutions--one that is actually quite efficient and can be mechanically executed. Essentially, rather than trying to eliminate the quantifier, it tries reducing the type, and the body bound by it. A key point is that this mechanism isn't special-cased for the "specification" parts--it's exactly the same reduction mechanism used everywhere in the program, and indeed it's very important for conversion that reduction behave this way. Thus, you can indeed efficiently, mechanically execute a type in Coq. Once it reaches normal form, of course, you can't perform any more reduction--but from the Coq kernel's perspective, up to eta conversion, types in normal form are distinct from an enumeration of all their inhabitants, meaning it is indeed doing the right thing here.
In other words: Coq does not allow you to only program with non-type terms, and it doesn't make a clean distinction between inhabitants of types and types themselves. Moreover, while for quantified parts this isn't usually that interesting, for nondeterministic parts (such as match expressions on unknown variables) it can actually be quite important; for example, dependent elimination within the return type of a match clause can determine the index of a value of an inductively defined type, thus actually affecting program execution (and vice versa, of course; for instance, a type can be constructed representing n iterated lambdas, where n is an unknown value that may either be specified at runtime or at compile time. It is this latter case that gives rise to techniques like proof by reflection that may approximate an exhaustive search in order to produce a proof object--but they do so because the user wrote a program specifically to do exhaustive search, not because there's some exhaustive search mechanism built into the language).
Yes, but I don't think anyone considers a SQL join to be a description of a linear-time algorithm.
> Coq executes what you term the specification parts in a very different way than trying to exhaustively enumerate solutions--one that is actually quite efficient and can be mechanically executed.
I never said you always need to exhaustively enumerate solutions. Nevertheless, the problem of extracting a computation from a specification (e.g., an inhabitant from a type) is undecidable in general[1]. Hence, specifications cannot be generally compiled, therefore they are not programming languages.
They could be a new kind of programming language, where some search algorithm could sometimes find a computation, but that would be a "programming language" in a completely different sense; Lamport does acknowledge that possibility (I know some people are researching program generation, but the results so don't look very promising, and in any event no one expects them to ever be more than heuristic, even if they're ever effective).
[1]: I'm not sure what happens if you know the type is inhabited. I guess it will be decidable in that case (just as finding a proof of a proposition that's known to be a theorem), but the search is still intractable, and there is no way the resulting computation would be efficient.
This is the first mention either of us have had of "linear-time" outside of a discussion about specifications. There aren't many programming languages that only let you write linear-time algorithms, and I think that's very far from most people's definition of a programming language. That being said, it's not like you can't write linear-time algorithms in Coq; its reduction machine is pretty efficient w.r.t algorithmic complexity (and it's likely to gain native machine integers and arrays soon to bring the constant factor in line with this). Proving linear-time execution for a native Coq function is another question entirely, of course, but you can always model a specific reduction machine in Coq and analyze that instead.
> Hence, specifications cannot be generally compiled, therefore they are not programming languages
I really don't agree with you on this. You have a fixed notion in your head if what it means to compile a type (attempt to find an inhabitant), but that is not how Coq interprets types at all; from its perspective, types are terms of independent interest, and are moreover themselves inhabitants of some other type. We don't expect a program to try to "find the inhabitant" of a term of type boolean when it's compiled; we want to keep reducing the term until it's in normal form (and, hopefully, our theory is consistent so it will be either true or false). In Coq, the same sort of reasoning (more or less) applies to types; it just keeps reducing it until it reaches normal form. There's no special notion of "finding an inhabitant" as distinct from normal program execution, which is exactly why I claim that Coq does not make the "specification-program" distinction. I'm not sure if I can explain it any more simply. I am not saying this is not a meaningful distinction in TLA+, or that it's not a real concept, but it's not the only way of thinking about things.
> I'm not sure what happens if you know the type is inhabited. It might be decidable in that case (just as finding a proof of a proposition that's known to be a theorem), but the search is still intractable, and there is no way the resulting computation would be efficient.
Depends on the problem. In Coq, for decidable problems you can write a decision procedure that is tailored to the individual type, having it produce a proof of the proposition you desire as a byproduct (in fact, in general producing such a procedure is how you prove that the problem is decidable!). Sometimes executing it is tractable and sometimes it isn't, but I don't agree that writing an algorithm to solve such a problem automatically transforms your domain from "efficient, everyday programming" to "ineffecient, specification-driven programming." Moreover, a lot of the time, there will be an easy inefficient decision procedure and a much harder efficient one, but given that they're both written in the same language and solve the same problem it seems hard for me to imagine that one would be considered "ordinary programming" and the other "program extraction" or whatever.
(In response to your [1], tactic languages like Coq's Ltac, much maligned as they are, are basically an attempt at interactive program synthesis; people rarely write complicated proof terms by hand. So I'd say these ideas have been a success, though hardly an unqualified one. Of course, one can argue that it's not "really" synthesis because you're not synthesizing the whole program from nothing but the specification, but even in ordinary program synthesis most successful solutions are based on sketching, where a partial program is provided and the synthesis engine fills in the gaps).
I mentioned it before, and my point isn't about linear time in particular. If you write a specification of an algorithm of time complexity T(n), the expectation is that interpreting the algorithm would take p(T(n)), where p is some polynomial (i.e. no exponential slowdown or worse). This is what I mean by "efficient".
> but that is not how Coq interprets types at all; from its perspective, types are terms of independent interest, and are moreover themselves inhabitants of some other type.
That doesn't matter. I can specify a function by giving it a type -- say it's a function from the even naturals to their Goldbach pairs. Turning this into a program requires finding a lambda term that computes such a function.
> There's no special notion of "finding an inhabitant" as distinct from normal program execution
What I meant was that a type in Coq is not a computation (although it could be the result of a computation), and a computation is not a type (although it could produce a type -- Pi types).
> I am not saying this is not a meaningful distinction in TLA+
In TLA+ there is no such distinction because you cannot talk about a program that computes that function, but always the set of all programs that do (you can, of course, give more and more detail to restrict the set, i.e., create subtypes, but there is no "the computation"); that set is always either empty or infinite. In fact, if it's non-empty, it's always too big to even be a set (it's a proper class).
> Sometimes executing it is tractable and sometimes it isn't, but I don't agree that writing an algorithm to solve such a problem automatically transforms your domain from "efficient, everyday programming" to "ineffecient, specification-driven programming."
I am not talking about writing an algorithm to solve such a problem automatically, but about a programming language that always does so.
> So I'd say these ideas have been a success, though hardly an unqualified one.
They have been an abysmal failure when it comes to synthesizing anything that could be considered a replacement for programming. But we're talking about two radically different measures of success. I'm talking about a commercial process of turning lead into gold, and you're talking about turning a couple of lead atoms into gold atoms in a particle accelerator.
What algorithm? There are many algorithms that inhabit the same type. A specification that's detailed enough to be able to analyze its complexity is usually a program... and it's easy to write a program that runs in linear time in Coq.
> That doesn't matter. I can specify a function by giving it a type -- say it's a function from the naturals to their Goldbach pairs. Turning this into a program requires finding a lambda term that computes such a function.
In Coq, you cannot specify a function by giving its type. First, CiC is not an extensional type theory in general; it cares about how things are computed, not just what the answer is. Secondly, for many interesting function types in Coq, there are an infinite, or even uncountable, number of inhabitants (for example : Prop -> bool). Moreover, in Coq's core type theory, even if it could automatically find all lambda input-outputs pairs that inhabited some type, that would not be justification to replace the quantified type (you need to assume the function extensionality axiom if you want this).
> I didn't say there was. What I said was that a type in Coq is not a computation, and a computation is not a type. Just as a proof is not a proposition and a proposition is not a proof.
A type in Coq is no more or less a computation than a term is. I don't understand what this has to do with "specification vs programming." As for "a proposition is not a proof", I think that is the main point of significant disagreement between us. Why do you think True doesn't prove Prop, for instance? It may not be the most interesting proof in the world, but neither is the proof I of True (and in many cases, proofs of Prop are very interesting in themselves, particularly in the context of dependent elimination).
> In TLA+ there is no such distinction. You cannot talk about a program that computes that function, but always the set of all programs that do (i.e., just the type).
Okay, then neither of them have such a distinction. What you seem to be missing is that in Coq, the mechanism for manipulating types is not different from the mechanism for ordinary program evaluation; it looks like TLA+ uses an axiomatic formulation rather than computation rules, so if you were to add evaluation to TLA+ you'd probably need a new set of semantics, but that's not the case for Coq.
> I am not talking about writing an algorithm to solve such a problem automatically, but about a programming language that always does so.
As you noted, such a programming language is impossible, so I don't understand why you are talking about it. The impossibility of that hypothetical programming language doesn't mean you can't write a single unified programming language (without two different "parts") that also functions as a specification language, and I genuinely don't understand why you think it does.
> They have been an abysmal failure when it comes to synthesizing anything that could be considered a replacement for programming.
The state of this has been steadily improving! For example, https://www.cs.utexas.edu/~isil/sypet-popl17.pdf looks quite promising for everyday programming tasks.
Not necessarily, and I would claim that it usually isn't, but to see that you have to pay close attention to how algorithms and systems are specified. I give the example of the QuickSort algorithm at the beginning of this post: https://pron.github.io/posts/tlaplus_part3
> In Coq, you cannot specify a function by giving its type.
Of course you can; that's the meaning of the type -- it's just not enough to get a computation. That's precisely the point I was getting at. A specification is a description of something at some arbitrary level of detail, but languages that allow compilation -- i.e. programming language -- normally require a minimum level of detail for that to be possible. In a language like Coq, this requirement is a strict syntactic distinction between types and lambda terms.
> First, CiC is not an extensional type theory in general; it cares about how things are computed, not just what the answer is.
Precisely. This is absolutely necessary for a programming language, and undesired in a specification language. (BTW, in TLA, what and how is arbitrary, because the temporal logic lifts everything that in Coq is operational into the denotation)
> A type in Coq is no more or less a computation than a term is.
A type is not a computation. To "run" something, or to speak of the operation of something, that something must be a lambda term.
> the mechanism for manipulating types is not different from the mechanism for ordinary program evaluation
I know that (I don't know Coq, but I know a bit of Lean, which is similar, I think), but that doesn't matter. You can compute with types, but there is a strict distinction between the common form of nonderterministic specification -- types -- and actual computation (not types).
> As you noted, such a programming language is impossible, so I don't understand why you are talking about it.
Because we're trying to work out the difference between a specification language and a programming language. A programming language is one that, when it describes a computation, can always be interpreted efficiently in the sense I meant. A specification language should allow specifying computations at arbitrary levels of detail. I claim that a specification language cannot be a programming language and vice versa -- except if we had this magical language I described. What you can do, and Coq does, is combine two languages in one, but even then the result requires a delineation between a computation and a specification (arbitrary nondet).
> For example, https://www.cs.utexas.edu/~isil/sypet-popl17.pdf looks quite promising for everyday programming tasks.
I honestly do like the research, but this is going from converting two atoms of lead into gold in a particle accelarator to five, or like saying that Olympic high jumpers are steadily improving in jumping all the way to the moon... This is another discussion, but I like the research and I like the practice, but I don't buy the claims that such improvements in research put changes to practice on the horizon. The gap is still huge, and I also think some of the research (especially in programming language theory) is done based on assumptions that completely fail in practice (I wrote about that here: https://pron.github.io/posts/people-dont-write-programs)
Math as a language is just a DSL which carries a lot of historical burden that is not friendly at all. Programming languages can achieve same level of abstraction with more clarity. Math instead added too much specific syntactic sugar(bad is multiply(b, a, d), log a is log(10, a) or log(e, a)), operator overload (/ for divide and dy/dx for differentiation operator, same grammar for scalar and matrix multiplication, one of which is communicative while the other is not), and complicated design (integral would be much clearer if we write integrate(target=ax, over=x, from=0, to=10) instead of the original one).
Maybe you prove your algorithms and call it a day, or maybe you can ask your program to run it, like an external dependency.
It's very unclear how TLA+ is neither programming or how it fits in with your programming. But he is not asking you to do normal math notation.
You can do that, or check it with a model checker (which is much easier). Either way, you verify your algorithm rather than "run" it (although the model checker lets you simulate or "run" a random execution).
For a "complex" problem[1] you cannot write a unified field definition[2] before the fact. Otherwise the problem would have to be merely complicated (most sufficiently useful systems are complex). The easiest way humans can make sense of a complex problem is to define a set of misfits[2], or tests. In practice efforts to find a better way of expressing the hidden algorithm of any given software system have failed. Yet "tests" have proven themselves as a sustainable way for humans to iteratively arrive at the most suitable solution to a complex problem and to guide understanding after the fact.
tl;dr a more elegant programming language is nice but does not solve the fundamental problem with human minds and solving complex problem domains
0: http://www.codecodex.com/wiki/Euclidean_algorithm
1: Cynefin, Dave Snowden
2: Notes on the Synthesis of Form, Christopher Alexander
TLA+ certainly allows you to describe a system as a set of scenarios/properties (what I assume you would call tests), and also of asserting that a design satisfies them.
There was a system I worked on that was so complex that I was only able to design it using TLA+; engineers at Amazon, Microsoft, Oracle and Intel report similar experiences.
It's all they know how to use because it's the only thing that actually works to produce results they need with minimal pain.
And you might not need to program in LaTeX, but everyone has their custom macros.
Word really hasn't changed that much.
Also, the rest of your comment doesn't make any sense, either.
A comment about the things you think he's more famous for doesn't make sense. A comment about LaTeX not being turing-complete, and citing as proof that it's largely a bunch of macros written in a turing-complete language (glued together with that turing-complete language) doesn't make sense either.