Live data from Hacker News

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

youtube.com

161–170 of 288 posts

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

#161
post #155

Earlier quoted context omitted.

> 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 le…

My point is that there are models of (essentially) Coq where there is no distinction between types and terms; both are translated into sets, in a fairly straightforward way. Additionally, one of the major points of dependent type theory is that reduction can occur anywhere, including directly within a type; i.e. term and type cannot be defined separately from one another. I'll go further and say that the fact that a term can only inhabit a type is in some sense definitional, since types are also terms; I can quite easily perform reduction and programming in a term that includes quantifiers, which you would say was part of the nondeterministic type level (in other words, terms do inhabit other terms). So it is extremely unclear to me that the distinction you are making is fundamental.

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

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

#162
post #106

I wasn't exposed to spreadsheets until a few years into college back around 1996 or 1997 maybe (I had been programming in C/C++ for 7 or 8 years by then). I wasn't taught matrix math until pretty late in the curriculum, I want to say junior or senior year. Also I was lucky to have a semester of Scheme but they were transitioning to teaching Java around the time I graduated (I don't know if they ever switched back). A…

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.

A ton of problems in software engineering, I am convinced (and isn't wild generalization one of the marks of our field! I at least want to own my own hypocrisy here) are communication problems. Nearly all the interesting ones, anyway.

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.

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

#163
post #155

Earlier quoted context omitted.

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 le…

My point is that there are models of (essentially) Coq where there is no distinction between types and terms; both are translated into sets, in a fairly straightforward way. Additionally, one of the major points of dependent type theory is that reduction can occur anywhere, including directly within a type; i.e. term and type cannot be defined separately from one another. I'll go further and say that the fact that a…

[deleted]

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

#164
post #155

Earlier quoted context omitted.

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 le…

My point is that there are models of (essentially) Coq where there is no distinction between types and terms; both are translated into sets, in a fairly straightforward way. Additionally, one of the major points of dependent type theory is that reduction can occur anywhere, including directly within a type; i.e. term and type cannot be defined separately from one another. I'll go further and say that the fact that a…

> My point is that there are models of (essentially) Coq where there is no distinction between types and terms

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

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

#165

Earlier quoted context omitted.

The problem is, most of the people who you are working with, only have 0-2 years of experience in the technology that they are using (use of research / deep learning to build products). Look at their resumes. They'd be either recent PhD grads, who haven't built a single product in their life. Or traditional engineers who had just joined the field of building products with an approach that is very different from one t…

That's an institutional problem though. 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 natura…

I'm finding a fifteen years figure hard to believe. There was a handful of people at that time that have invented deep learning. It took years to get any industry use, as the technology was not yet competitive, until AlexNet.

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

#166
post #162
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.

A ton of problems in software engineering, I am convinced (and isn't wild generalization one of the marks of our field! I at least want to own my own hypocrisy here) are communication problems. Nearly all the interesting ones, anyway. 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 ex…

Yeah, interestingly, I have this impression that Python is a modern-day Fortran. (Largely for the reasons you describe in the third category of programmers.)

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

#167
post #9

A summary of the article the talk was based on and some discussion on this. http://muratbuffalo.blogspot.com/2018/07/if-youre-not-writin...

"It's quite likely that during their lifetime, machine learning will completely change the nature of programming." - Why is this the case? Even if it's true, it hardly seems obviously true.

I recall hearing some thing similar around 1980 :-)

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

#168

I wasn't exposed to spreadsheets until a few years into college back around 1996 or 1997 maybe (I had been programming in C/C++ for 7 or 8 years by then). I wasn't taught matrix math until pretty late in the curriculum, I want to say junior or senior year. Also I was lucky to have a semester of Scheme but they were transitioning to teaching Java around the time I graduated (I don't know if they ever switched back). A…

"...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"

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.

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

#169

Earlier quoted context omitted.

>Honestly I think it might be time to phase out teaching imperative and object-oriented programming. 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".

It triggers me to no end when I watch an introductory course, for people with no previous exposure to any programming language, and the teacher starts with "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…

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

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.

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

#170
post #162

Earlier quoted context omitted.

A ton of problems in software engineering, I am convinced (and isn't wild generalization one of the marks of our field! I at least want to own my own hypocrisy here) are communication problems. Nearly all the interesting ones, anyway. 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 ex…

Yeah, interestingly, I have this impression that Python is a modern-day Fortran. (Largely for the reasons you describe in the third category of programmers.)

On some level that's literally true: when you run NumPy or SciPy code, most of your basic array manipulations are done by BLAS, which are a set of very tightly optimized linear algebra routines originally written in Fortran.
Post reply on HN