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

I want to fix programming

jonbho.net

Post reply on HN
Print view View original

61–70 of 163 posts

Re: I want to fix programming

#61

Post by _sh »

AUmrysh wrote: post #41
Tuna-Fish wrote: post #32

Earlier quoted context omitted.

Declarative languages are defined by the fact that in them, you don't tell the compiler how to do things. You just describe the result you want, and it's the compilers job to get there. Yes, this makes the compiler rather hard to write. SQL is probably the primary example. Prolog is also well-known.

For anyone who may not know, Prolog does this in a pretty interesting way. You have some declarations that make up your program, Prolog takes these and then uses them to conduct a logical proof (like in discrete math). You negate the premise (proof by contradiction), and then try to show that this will cause a contradiction (line 5 says Bob is Human, but line 42 says Bob is not Human). If you can find such a contradi…

Also fascinating is the amazing and innovative virtual machine that drives Prolog: the Warren Abstract Machine.

See: http://wambook.sourceforge.net/

Re: I want to fix programming

#62

Post by iso8859-1 »

dxbydt wrote: post #53

I once read a programming book on Elliptic Curve Cryptography, which was invented by Dr. Neal Koblitz. So the book said - whatever is in the next 200 pages is considered trivial by mathematicians working in number theory. If you write it in the form of equations, this entire book will occupy less than half a page. It is basically a lemma and a few theorems. But this book is 200 pages long. Why ? Because it tells you…

I imagine that the book might as well have used another (simpler) language. Now, as I see it, to understand the math, you need quite a lot of domain knowledge. A formula doesn't make sense out of context. Most statements written in programming languages do that, in a much higher degree.

Therefore, to actually do the ECC, I think it's quicker just to read the language specification of your (simple) language, than actually understand all of the math being the formulas. Granted, you wouldn't understand WHY it works. And that's my point. Comparing math to programming languages is like comparing apples to oranges.

Re: I want to fix programming

#63

Post by Peaker »

jng wrote: post #22
raganwald wrote: post #10

Dear Jon: What you have is fabulous and immediately useful: You are describing a language for describing constraints on the results of computer programs. In other words, you can express the correctness of a computer program and check whether a program is, in fact, correct. It’s true that IF a sufficiently smart compiler could infer a working program from the definition of correctness, no further “programming” would b…

Reg, thanks so much for your comment. I'm really happy you appreciate the value. It's very interesting that you put the focus in the descriptive language. I've been working on that for a long time. It's not finished, but some areas are clarified. Indeed, after reading your comment I think I will try to focus on getting somewhere workable with that part first. This whole project is so big. It will be good to do it in…

The "Why Dependent Types Matter" paper at http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf actually uses an implementation of "sort" as its driving example.

The paper starts out with a simple sort implementation, and then adds static proofs of correctness for:

A) Totality (Termination/no infinite loops) B) Length of output = Length of input C) Output is sorted

It does not prove the one-to-one mapping, and I don't know how hard that would be to prove (intuitively, it does not sound like it should be too hard).

The dependent types approach lets you write a program while reasonably controlling its algorithmic complexity and operational behavior -- and still have its mathematical meaning proven to match a specification.

I think a title like "I want to fix programming" is a bit over the top -- given that it is a hard problem with very smart people working at it. It is more acceptable, in my opinion, to "fix programming" after learning in detail what the state of the art already entails. That means knowing Agda, Coq, Logic languages, Hoare logic, etc.

Re: I want to fix programming

#64

Post by ChristianMarks »

The problems the OP wants to solve are formally undecidable and reducible to the halting problem.

1. Given a formal specification, find a program that meets the specification.

2. The apparently simpler problem of checking whether a given program meets a specification.

Both are undecidable. That said, there is an extensive literature on practical approaches to this problem. They generally suffer from intractability.

http://cfpm.org/pub/papers/tiofdm.pdf

I suggest looking at Robert Harper's book on type theory instead.

Re: I want to fix programming

#65

Post by andrewcooke »

ezyang wrote: post #50

Here is another way of defining something is sorted, taken straight from a real language: Inductive StronglySorted : list A -> Prop := | SSorted_nil : StronglySorted [] | SSorted_cons a l : StronglySorted l -> Forall (R a) l -> StronglySorted (a :: l). What this says is that an empty list is sorted (SSorted_nil), and that given some sorted list l, if a is less than all of the elements in l (well, we generalize to som…

http://www.cis.upenn.edu/~bcpierce/sf/ is a good way to learn coq if you are interested and don't already know it.

also, i didn't completely follow the final example, but you might find that category theory is relevant. related, it's not completely clear to me why you're not happy with functional programming. in a sense what academic functional programmers are doing is what you want your software to do. they're just not smart enough to put it in a compiler yet. i think. for example http://www.fing.edu.uy/inco/cursos/proggen/Articulos/sorting... (isn't that kinda what you want?)

Re: I want to fix programming

#66

Post by protomyth »

espeed wrote: post #36
protomyth wrote: post #28

The most common declarative programming language used in SQL. In theory the optimizer takes my declaration and builds an optimum (or at least decent) set of step in the database engine to accomplish what I have declared. With all the work in this limited area, database optimizers get it really wrong quite a lot (Sybase 12.5 was bad enough on big data that forcing order of joins and indexes was needed). I am not sure…

The most common declarative programming language used in SQL. Or maybe a spreadsheet ( http://philip.greenspun.com/panda/databases-choosing ).

although I respect Philip Greenspun greatly, most spreadsheets I have seen are pretty procedural. People tend to think in steps on those types of calculations.

Re: I want to fix programming

#67

Post by philh »

My question: what can this not solve? What problems could a human solve that this language couldn't?

I think that would help me get a better idea of what you're trying to accomplish.

Re: I want to fix programming

#68

Post by DenisM »

The quality of the comments both here and the author's blog is astonishingly good, every comment adding something to the discussion. This is the hacker news I know and love.

Re: I want to fix programming

#69

Post by DannoHung »

You have to define the way that the sort should work though, and at that point, what you really want is functional dependencies. Coq, Idris, Agda, etc, etc.

Not a lot of fun to learn how they work, but they're really quite impressive.

Re: I want to fix programming

#70

Post by koko775 »

Sounds like a combination between flow-based programming and declarative programming. Perhaps a possible approach would be to write a flow-based programming language with some methods marked as "pure" which statelessly map input to output and others able to be written in a more traditional, imperative, less functional style?

In a flow-based architecture, it seems to me that by design, almost every component in the flow would be testable.

Post reply on HN