Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A Path to Enlightenment in Programming Language Theory

steshaw.org

Post reply on HN
Print view View original

91–99 of 99 posts

Re: A Path to Enlightenment in Programming Language Theory

#91

Post by ufo »

xjia wrote: post #65
sgeisenh wrote: post #64

Earlier quoted context omitted.

Check out compcert for a verified c compiler. And several Haskell projects have been verified.

I know it is possible. But I wonder what stops us from doing it for most programs we write from day to day. And, if proving correctness is indeed important (I believe so), can we do something / what is the next thing to do to enable us proving correctness in our daily job.

For an example of what mafibre is talking about: even proving that a BubbleSort implementation is correct is quite tricky.

First of all, you need to correctly define the specification. Saying "the returned list is sorted" isn't enough because that would also accept lists that have nothing to do with the input, like [1,2,3,4,5]. Also saying that the list only contains elements from the input is also not enough because that would accept a returned list with duplicated or missing elements. To really make a specification that models what you want you need to say that the returned list is a sorted permutation of the input list.

Then, once you manage to get a formal specification that is actually what you want prout invariantving it is also hard. In the bubble sort case you need to figure you need to write down the proofs in detail, down to the point when you use the fact that comparison is a transitive relation.

Re: A Path to Enlightenment in Programming Language Theory

#92

Post by nbouscal »

dschiptsov wrote: post #89
nbouscal wrote: post #81

Earlier quoted context omitted.

... You know that we do have a categorization of clouds, right? I think meteorologists would disagree with you about the utility of that categorization. More to your point: whether you can do something without a tool has no bearing on whether or not it is a useful tool. You can write programs in machine code if you'd like to, but you're highly unlikely to be as productive as someone using a high-level programming lan…

Except when the type system restricts you to homogeneous data-structures in inherently heterogeneous world. Herbert Spencer, the philosopher, could tell us a lot about it. As for crude and misleading clasdification - there is no shortage for them, especially in realms of psychology (hypohondric, sangvinic - all that nonsense) or economics and finance. The results of application of flawed economic/financial models bas…

http://chrisdone.com/posts/existentials

Re: A Path to Enlightenment in Programming Language Theory

#93

Post by nbouscal »

JesperRavn wrote: post #83
nbouscal wrote: post #82

Earlier quoted context omitted.

I've spent a lot of time hanging out with pretty hardcore type theory people, and have never seen any of them recommend a dependently-typed language to a new programmer. In other words, you're pretty blatantly fighting a straw man.

It's not about how experienced the programmer is. The problem is that people do a bate and switch when it comes to type theory, promising the benefits of dependent types even though there are no production languages that deliver these benefits.

I've similarly never seen anyone promise the benefits of dependent types when talking about simpler type systems. Why would they need to? Much simpler type systems already have more than enough benefits to be worthwhile.

I'm not actually looking to debate you, your mind is made up and there's very little chance I'll change it, not that it would matter if I did. I mainly just want to point out for others reading this that your arguments are blatant straw men.

Also just fyi, it's "bait and switch".

Re: A Path to Enlightenment in Programming Language Theory

#94

Post by JesperRavn »

nbouscal wrote: post #93
JesperRavn wrote: post #83

Earlier quoted context omitted.

It's not about how experienced the programmer is. The problem is that people do a bate and switch when it comes to type theory, promising the benefits of dependent types even though there are no production languages that deliver these benefits.

I've similarly never seen anyone promise the benefits of dependent types when talking about simpler type systems. Why would they need to? Much simpler type systems already have more than enough benefits to be worthwhile. I'm not actually looking to debate you, your mind is made up and there's very little chance I'll change it, not that it would matter if I did. I mainly just want to point out for others reading this…

>Much simpler type systems already have more than enough benefits to be worthwhile.

If that's your opinion, why did you ignore the fact that I addressed this in my original post? You accuse me of having a straw man argument, and yet you can't even engage with what I've written?

Anyway, you're right that neither of us is likely to convince the other, but I have really seen arguments that go like the one I described, and you're really doing me a disservice by ignoring the details of what I posted.

Re: A Path to Enlightenment in Programming Language Theory

#95

Post by dllthomas »

Silhouette wrote: post #21
exDM69 wrote: post #17

Earlier quoted context omitted.

> knocking together a small lambda calculus + dependently typed interpreter in C. Not ML, Not Ocaml, not, Haskell, not any language that is _already_ got lambdas in it! This wouldn't be any more educational and just plain painful. "Research" programming languages tend to work very well for building compilers, that's why they are used in many toy programming language projects. Dealing with tree and graph structures in…

The flip side of this is that if you're writing something in C, you actually do have to understand how details like closures are implemented on real hardware. These are not trivial problems, yet many programming language design papers and articles effectively brush the whole issue of actually implementing these things under the carpet. Go ahead and search for that particular example. There is almost nothing on the We…

You're confusing levels. If you are compiling to C or assembly, you have to understand how the constructs you are building work. That places no requirement on the language of implementation of the compiler.

Re: A Path to Enlightenment in Programming Language Theory

#96

Post by Silhouette »

dllthomas wrote: post #95
Silhouette wrote: post #21

Earlier quoted context omitted.

The flip side of this is that if you're writing something in C, you actually do have to understand how details like closures are implemented on real hardware. These are not trivial problems, yet many programming language design papers and articles effectively brush the whole issue of actually implementing these things under the carpet. Go ahead and search for that particular example. There is almost nothing on the We…

You're confusing levels. If you are compiling to C or assembly, you have to understand how the constructs you are building work. That places no requirement on the language of implementation of the compiler .

Yes, but IME many tutorial presentations on these subjects never get as far as actually building a complete, functional compiler to demonstrate the concepts. Often they use some form of interpreter instead, which means they can use structures in the interpreter's implementation language that somewhat reflect the run-time structure of the implemented language using the analogous language features.

Re: A Path to Enlightenment in Programming Language Theory

#97

Post by groovy2shoes »

jcurbo wrote: post #66

I spotted this on Twitter [0] and it was timely for me because I've been sorta building my own learning path lately. After learning Haskell a few years ago I got really interested in PLT, type theory, and other higher math (like CT) and also things like formal program verification and automated solvers. So I started trying to decide on a good self-study path (as a guy with a day job who's not going to be starting a P…

Pinter's A Book of Abstract Algebra is one of the best math books I've ever read. It's short, to the point, and doesn't assume you're an idiot. I learned a lot from it and I can't recommend it enough.

Re: A Path to Enlightenment in Programming Language Theory

#98

Post by dllthomas »

Silhouette wrote: post #96
dllthomas wrote: post #95

Earlier quoted context omitted.

You're confusing levels. If you are compiling to C or assembly, you have to understand how the constructs you are building work. That places no requirement on the language of implementation of the compiler .

Yes, but IME many tutorial presentations on these subjects never get as far as actually building a complete, functional compiler to demonstrate the concepts. Often they use some form of interpreter instead, which means they can use structures in the interpreter's implementation language that somewhat reflect the run-time structure of the implemented language using the analogous language features.

Well, it makes sense for tutorials to use what they can to simplify the bits they're not focusing on, but certainly implementing a construct by mapping it into an identical construct is not going to be terribly informative as to the workings of that construct. That may be totally appropriate if the focus of the tutorial is on the parsing or such, but it sounds like that sort of tutorial (of which there are many, and which are perfectly useful to other purposes) are not what you are looking for.

Re: A Path to Enlightenment in Programming Language Theory

#99

Post by nbouscal »

JesperRavn wrote: post #94
nbouscal wrote: post #93

Earlier quoted context omitted.

I've similarly never seen anyone promise the benefits of dependent types when talking about simpler type systems. Why would they need to? Much simpler type systems already have more than enough benefits to be worthwhile. I'm not actually looking to debate you, your mind is made up and there's very little chance I'll change it, not that it would matter if I did. I mainly just want to point out for others reading this…

>Much simpler type systems already have more than enough benefits to be worthwhile. If that's your opinion, why did you ignore the fact that I addressed this in my original post? You accuse me of having a straw man argument, and yet you can't even engage with what I've written? Anyway, you're right that neither of us is likely to convince the other, but I have really seen arguments that go like the one I described, a…

You "addressed" it by referring to "studies" that you didn't cite. There are studies that go both directions on the question, none of which have good enough methodology to be worth more than a tiny update in either direction. Most of the studies are about extremely weak type systems (C, Java, etc.), and therefore don't provide any evidence at all about type systems that are stronger than Java but weaker than dependent types (e.g. Swift, Rust, Haskell, etc).

Meanwhile we have a lot of people who have used both weak type systems and strong type systems who claim that strong type systems make their jobs dramatically easier, and we have a lot of people who have only used weak type systems who claim the opposite. Take a survey of people who have actually done non-trivial work using a language with a good type system, and you'll get very clear results about their view of the benefits. Clearly an RCT would be better, but given that training takes a long time, that just isn't feasible.

Post reply on HN