Live data from Hacker News

If You're Not Writing a Program, Don't Use a Programming Language [video]

youtube.com

151–160 of 288 posts

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#151
post #126
post #117

Earlier quoted context omitted.

Since when is it a requirement that a programming language be efficient? 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,…

> Since when is it a requirement that a programming language be efficient? 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…

> No programming language can do that (i.e. describe non-computable "algorithms")

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!).

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#152
post #122
post #106

Earlier quoted context omitted.

Computers are still imperative, so all functional code is arguably syntactic sugar over that core causing a lot of leaky abstractions to show up all over the place. 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.

I have heard critiques of functional programming, but not that there is a problem with leaky abstractions. Can you provide an example? Does it invalidate the discipline of trying to use pure functions when possible? 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 ad…

Purely functional languages come with the promise that a sufficiently advanced compiler will see through all that monadic functional cruft and run your code as well or even better than it would if written in an imperative language.

As we don’t yet have such an advanced compiler, impure hacks like `par` start seeping through the cracks.

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#153
post #59

Earlier quoted context omitted.

I think that tools such as TLA+ show their value not by convincing people that they're worth the extra effort but that they actually save you effort. The experience at Amazon and Microsoft shows exactly that, and managers were relatively easily convinced.

Absolutely agree. I work in the autonomous vehicle space, specifically in creating high-assurance resilient systems, and I've had more arguments that I care to count which went something like the following: 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 al…

I think your frustration largely arises because the problem you work on is uncommon. The goals you are working towards are very large and error is not an option because people die or at least massive property damage occurs. Most applications aren't like that. It doesn't matter much if 1/10k image upload to Instagram fail. We have a lot more Instagrams than autonomous cars so the engineering culture conversion is largely dominated by those trade offs. It's interesting because I think we see experiencing the pendulum having swung heavily towards Agile. In the past we used to slow down some crud apps by first drawing UML diagrams. Fingers crossed that we can discover a wider, more differentiated range of engineering practices.

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#154
post #150

Earlier quoted context omitted.

> Distinction between dynamically typed and statistically typed is clear. 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.

That's completely abstract example, not relevant to actual practice. It's hard for actual programmer make that mistake.

It's a concrete example, but I understand your point that "in practice" we know what dynamic vs. static typing means. Personally, I think a lot of that just comes down to marketing, though :)

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#155
post #126

Earlier quoted context omitted.

> Since when is it a requirement that a programming language be efficient? 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…

> No programming language can do that (i.e. describe non-computable "algorithms") 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 progr…

Typed programming languages (any typed formal systems, for that matter) are made of two languages, type level and term/object level. While the two are strongly related, they are separate (a term can inhabit a type, but not another term). The level of nondeterminism required for specification exists at the type level and not at the term level, while programming (in the sense I defined above) exists only at the term level. This is what I meant when I said above that a specification language can be embedded into a programming language (this doesn't require types, but can also be done with contracts), but those are still two languages, even if they share syntax. If you like, you can think of TLA+ as being entirely at the type level.

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#156
post #116

I'm more with Mike Acton in this respect; the hardware is the platform, not the software. And in that sense... In order to really make good use of your hardware you need to understand your hardware and code accordingly. I doubt you can achieve great performance on a language that focuses entirely on mathematical representations without considering the hardware. So yeah... you end up with a beautiful mathematical expr…

The problem with being too close to your hardware is that you become non-portable, or you create a situation where a CPU for a word processor becomes the dominant platform for decades. 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 assemb…

I agree with some of the things you say... mostly with the "use the right tool for the right job". In that sense, C might not be the most sensible choice for some things where you can end up with a solution that is twice as slow or more (and it's acceptable) but a lot easier to code and maintain. But if it several orders of magnitude slower? ... I just used C as an example of something that is obvious to reason about when comparing the alternative.

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.

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#157
post #148
post #132

Earlier quoted context omitted.

Program execution time and memory footprint are great examples. Math does not care about these details, but just because two programs are logically equivalent does not mean they will behave identically. 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.

That's a curious place to draw the line. As we've seen in the past year, assembly isn't good enough. You need to understand your microcode or it will eventually bite you ... and you don't. 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 sa…

The best example I can give is not quite functional code. I have seen a lot of horrific SQL because someone did not really understand that Joins for example had a cost based on some understandable criteria. You need to have a basic mental model of what the database does to write good SQL.

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.

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#158
post #59

Earlier quoted context omitted.

I think that tools such as TLA+ show their value not by convincing people that they're worth the extra effort but that they actually save you effort. The experience at Amazon and Microsoft shows exactly that, and managers were relatively easily convinced.

Absolutely agree. I work in the autonomous vehicle space, specifically in creating high-assurance resilient systems, and I've had more arguments that I care to count which went something like the following: 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 al…

Either your frustration is great, or you have the mind of a jedi. This is without a doubt the most scathing review I've read of agile, and you don't seem to even be trying.

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#159
post #21
post #3

I haven't watched the full talk, so let me know if this gets explored by Lamport, but... 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 signi…

>yet programmers tend to prefer untyped languages to typed languages 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…

I think most of the dynamic/static bias depends on the specific experiences of your problem domain.

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.

Re: If You're Not Writing a Program, Don't Use a Programming Language [video]

#160
post #30
post #3

I haven't watched the full talk, so let me know if this gets explored by Lamport, but... 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 signi…

Lamport would argue that if you're debating typed vs. untyped PLs, you're already missing the point, as all programming languages are necessarily [1] at a level that's too low for system/algorithmic thinking, and if you're working in a language appropriate to thinking about algorithms/systems, then the considerations surrounding typing are quite different from those pertaining to PLs (TLA+ happens to be untyped, but…

As I understand it, TLA may technically be untyped but that's simply because you are supposed to implement your own more granular type checking as part of your spec.
Post reply on HN