Hacker News Reader

Comment by raganwald | Hacker News Reader

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 be required. However, we don’t have that yet, and in fact I’m not urging you to write it.

Instead, consider the benefits of your language just the way it is. You can use it to write test suites. You can embed it in other languages to express design-by-contract.

It looks valuable in its current form.

View on HN

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 open and use as much help as I can.

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.

Thanks Peaker. I know a bit about dependent types, and how complex types sytesm can help a lot. Indeed, the title is a bit over the top (or maybe even too much over the top!). Hopefully the attention will help get some extra hands & brains.

At the very least, all the pointers I'm receiving are really valuable.

I don't claim I can fix it, but I definitely want to fix it, have some ideas, and I'm willing to work, listen and learn!

And if I think I can add something, is that I come from a practical/industrial background. Most of my work has been in C++. I'm looking for practical tools for everyday work.

Take a look at quickcheck if you want something that works today.

http://www.haskell.org/haskellwiki/Introduction_to_QuickChec...

Reply on news.ycombinator.com