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

61–70 of 99 posts

Re: A Path to Enlightenment in Programming Language Theory

#61

Post by ufo »

igravious wrote: post #28
mafribe wrote: post #16

Earlier quoted context omitted.

When I open Pierce TaPL and see immediately ML my heart sinks. I strongly recommend that you ignore this feeling and learn a modicum of ML coding. If you want to learn TAPL, just learn a bit of Ocaml. You don't need much. If you already speak C, a bit of Haskell and Ruby, you should be able to pick up enough Ocaml in a few hours/days. Programming in Ocaml is way easier than in Haskell or C. The only two things that a…

Really? I feel like C fits my brain, know what I mean? I don't even think that it was because I learnt it early on. It's a simple language, I feel. Why is programming way easier in Ocaml than in C? Setting aside that for me programming is way easier in C than in Ocaml because I know C and don't know Ocaml, what is it about Ocaml that is way easier than C? Anyway, my original point is that it is _cheating_ to explain…

Are you sure C is simpler then ML? If you really get into the nitty gritty details (which is what you do when interacting with programming language theory), the definition of the lambda calculus fits in a single page and an ML-lite that is powerful enough for real programming is just a little larger than that.

On the other hand, C needs a manual with hundreds of pages and has lots of dark corners and undefined behaviour. IMO, if you really want to keep things simple you need to stick to assembly language instead of C.

Re: A Path to Enlightenment in Programming Language Theory

#62

Post by xjia »

mafribe wrote: post #18
exDM69 wrote: post #13

Earlier quoted context omitted.

Because imperative programming is not very interesting from a programming language theory point of view. If this was a list about compiler construction, it would look very different. As we're seeing more and more language features originating from functional programming trickle into mainstream languages, this research hasn't clearly gone to waste even though everyone is not programming in functional programming langu…

imperative programming is not very interesting from a programming language theory point of view. I'm afraid I disagree, the opposite is the case. Modern PL theory is mostly about program correctness, and that is much easier for pure functional languages. Until recently, nobody had a handle on program logics for imperative languages, or reasoning techniques for operational semantics. The only available reasoning techn…

If program correctness is easy to prove, why we are not doing that when using either C or Haskell?

Re: A Path to Enlightenment in Programming Language Theory

#63

Post by AnimalMuppet »

ufo wrote: post #61
igravious wrote: post #28

Earlier quoted context omitted.

Really? I feel like C fits my brain, know what I mean? I don't even think that it was because I learnt it early on. It's a simple language, I feel. Why is programming way easier in Ocaml than in C? Setting aside that for me programming is way easier in C than in Ocaml because I know C and don't know Ocaml, what is it about Ocaml that is way easier than C? Anyway, my original point is that it is _cheating_ to explain…

Are you sure C is simpler then ML? If you really get into the nitty gritty details (which is what you do when interacting with programming language theory), the definition of the lambda calculus fits in a single page and an ML-lite that is powerful enough for real programming is just a little larger than that. On the other hand, C needs a manual with hundreds of pages and has lots of dark corners and undefined behavi…

You think that assembly needs less of a manual than C? You think assembly has less dark corners? You think it's going to make things simpler? My mind boggles.

Oh, and also, which assembler? 68000? x86? ARM? (One of these is not like the others in terms of complexity...)

Re: A Path to Enlightenment in Programming Language Theory

#64

Post by sgeisenh »

xjia wrote: post #62
mafribe wrote: post #18

Earlier quoted context omitted.

imperative programming is not very interesting from a programming language theory point of view. I'm afraid I disagree, the opposite is the case. Modern PL theory is mostly about program correctness, and that is much easier for pure functional languages. Until recently, nobody had a handle on program logics for imperative languages, or reasoning techniques for operational semantics. The only available reasoning techn…

If program correctness is easy to prove, why we are not doing that when using either C or Haskell?

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

Re: A Path to Enlightenment in Programming Language Theory

#65

Post by xjia »

sgeisenh wrote: post #64
xjia wrote: post #62

Earlier quoted context omitted.

If program correctness is easy to prove, why we are not doing that when using either C or Haskell?

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.

Re: A Path to Enlightenment in Programming Language Theory

#66

Post by jcurbo »

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 Ph.D. anytime soon). I ran across this very helpful Reddit thread [1] and so far I'm thinking of the following path. I'm starting with How to Prove It, because I never did a lot of proof solving in college (and that was >10 yrs ago anyway) and it's a good basis for further work. Then I have two branches.

The first is for abstract algebra and CT, because I find them interesting and they're useful for understanding Haskell, that currently consists of Pinter's A Book of Abstract Algebra, then Conceptual Mathematics by Lawvere and Schanuel, then Awodey's CT book, which is a path straight out of that Reddit thread.

The second is for PLT/type theory, and starts with Software Foundations by Pierce, then Types and Programming Languages by Pierce, then Practical Foundations for Programming Languages by Harper (for completeness, as I have heard pros and cons for both), then maybe moving to Advanced Topics in Types and Programming Languages and such. Mix in some Oregon Programming Language Summer School (OPLSS) [2] videos here and there when they fit. (OPLSS sounds great and I'm glad their videos are online)

[0] https://twitter.com/manisha72617183/status/61301658769664819...

[1] http://www.reddit.com/r/haskell/comments/29reb7/first_or_sec...

[2] http://www.cs.uoregon.edu/research/summerschool/

Re: A Path to Enlightenment in Programming Language Theory

#67

Post by mafribe »

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.

What stops us is cost. Formally verifying non-trivial properties (in the sense of CompCert) with current technology is several orders of magnitude more expensive and time-consuming than programming and a bit of testing. And this price is almost never worth it.

We hope that this cost can be lowered in the future.

Re: A Path to Enlightenment in Programming Language Theory

#68

Post by mafribe »

seanmcdirmid wrote: post #46
NotableAlamode wrote: post #40

Earlier quoted context omitted.

The semantics of OO languages is really messy and complicated and probably has the least well understood theory of all sequential forms of computing.

Not just that, but we still don't really know how to combine subtyping and generics very well. The soundness question when considering variance is still quite open, and it shows in the poor support for type inference in OO languages (in spite of heroic efforts made in languages like Scala). Much of this has to do with the root: most of our PL theory was basically designed for FP, and applying them to OOP has been pre…

I suspect that combining generics with subtyping might always lead you into the land on undecidable type-inference. After all, pure genericity (System F) is already undecidable.

Re: A Path to Enlightenment in Programming Language Theory

#69

Post by ufo »

AnimalMuppet wrote: post #63
ufo wrote: post #61

Earlier quoted context omitted.

Are you sure C is simpler then ML? If you really get into the nitty gritty details (which is what you do when interacting with programming language theory), the definition of the lambda calculus fits in a single page and an ML-lite that is powerful enough for real programming is just a little larger than that. On the other hand, C needs a manual with hundreds of pages and has lots of dark corners and undefined behavi…

You think that assembly needs less of a manual than C? You think assembly has less dark corners? You think it's going to make things simpler? My mind boggles. Oh, and also, which assembler? 68000? x86? ARM? (One of these is not like the others in terms of complexity...)

Maybe talking about undefined behavior wasn't the best approach I could take :) But if you stick to simple machine languages then it shouldn't be a big problem. Something that is closer to Knuth's MIX than to x86 won't have much undefined behavior.

The thing that I was thinking about was that many operations that are defined in assembly language, such as integer overflow are undefined in C (and this undefined behavior is often abused by optimizing compilers) and C also abstracts over a lot of control flow conventions.

Post reply on HN