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

Programming paradigms that change how you think about coding

brikis98.blogspot.com

Post reply on HN
Print view View original

91–100 of 206 posts

Re: Programming paradigms that change how you think about coding

#91

Post by sold »

JadeNB wrote: post #76
nuncanada wrote: post #67

Earlier quoted context omitted.

Yes, Depently Typed languages can. They are full blown theorem provers...

Gödel guarantees that full-blown theorem provers, even with human guidance, cannot prove all true statements about sufficiently rich systems. 'Sufficiently rich' here just means 'includes Peano arithmetic', and you can find tons of tutorials for doing just that (Church encoding) in even the simplest type systems. (This bit of pure-mathematics wonkery ignores the substance of jarrett's question, though; one doesn't ne…

When I write a program, I don't want it to be just correct (true); I want it to be _provably_ correct; I want to be able to be convinced that it is correct, at least in principle, given enough time and whole specification of the system. Programs which are correct, but not provably so, should not pass code review and might as well be lumped together with those which are wrong. It doesn't matter if you are using a full-blown theorem prover or thinking about the code in your head; Gödel's theorems are not really relevant to programming, even when the code uses deep mathematics.

I'm not sure I agree with "theorems that must be verified at compile time can never account for data that are provided only after compilation". At compile time, you prove the assertion "for every x, the program outputs correct answer for x". Now, you don't know that the user will enter say x=5 at runtime, but since you proved a theorem about _every_ x, this includes x=5. You cannot predict the future (the path that will be taken by the program), but once you prepare for all possible futures, you're safe.

Re: Programming paradigms that change how you think about coding

#92

Post by arh68 »

jarrett wrote: post #63

A thought on dependent types: Can a dependent type system catch all type errors at compile time? For example, suppose I write the following (in pseudo-code): // Variable x is an integer greater than or equal to 0 and less than 256. int x (>=0, I can imagine how a compiler could catch that kind of error. But that's trivial. What happens in programs like this: int x (>= 0, Now the compiler can't know for sure whether t…

> Can a dependent type system catch all type errors at compile time?

I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

> because the value of getKeyboardInput could be anything

That makes my brain hurt. I think implicitly narrowing the type is stylistically better. Maybe just adding a dependent type declaration:

    x = (parseInt(getKey) :: Int(>=0,
Then you type-annotate everything you can, marking every non-annotated expression as wild:

    w = ... :: Int(>=0, =0, =0,
Asking the compiler to infer arbitrary type declarations seems hard. I think y probably shouldn't be inferred as :: Int(0The work still needs to be done (no magic bullet here), but we should be able to use the computer to generate well-defined type combinations.

Re: Programming paradigms that change how you think about coding

#93

Post by arjunnarayan »

jarrett wrote: post #87
dllthomas wrote: post #75

Earlier quoted context omitted.

"Can a dependent type system catch all type errors at compile time?" Provably not, if you want a type checker guaranteed to finish.

Could you give a brief overview of why? Does this come down to the halting problem?

Basically, yes. If you want your type checker to be decidable, you're going to have to restrict the type language to be much smaller. In general, dependent types are undecidable to type check.

Re: Programming paradigms that change how you think about coding

#94

Post by hexagonc »

My first and only encounter with "Concatenative Languages" was programming the HP48GX[1] graphing calculator in highschool. Thinking back to it, I'm amazed by what you could do with it. It was very powerful even by today's standards. Whereas other kids had Gameboys, I had an "HP". I even got in trouble playing tetris on it during my German language class. My calculus teacher never knew that you could do symbolic integrals and derivatives with it (using a free computer algebra library). Sadly, the only program of note that I wrote for it was an implementation of the The Game of Life[2].

[1] http://en.wikipedia.org/wiki/HP-48_series [2] http://en.wikipedia.org/wiki/Conway%27s_Game_of_Life

Re: Programming paradigms that change how you think about coding

#95

Post by mnarayan01 »

arh68 wrote: post #92
jarrett wrote: post #63

A thought on dependent types: Can a dependent type system catch all type errors at compile time? For example, suppose I write the following (in pseudo-code): // Variable x is an integer greater than or equal to 0 and less than 256. int x (>=0, I can imagine how a compiler could catch that kind of error. But that's trivial. What happens in programs like this: int x (>= 0, Now the compiler can't know for sure whether t…

> Can a dependent type system catch all type errors at compile time? I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible. > because the value of getKeyboardInput could be anything That makes my brain hurt. I think implicitly narrowing the type is stylistically better. Maybe just adding a dependent type declaration: x = (parseInt(get…

> I'm probably not clever enough, but someone could probably prove that'd be equivalent to solving the halting problem. It seems impossible.

Guessing you're plenty clever...just didn't think about it enough :)

Simply transform a program into one which halts on a type error rather than whatever else it might be doing. Done.

Re: Programming paradigms that change how you think about coding

#97

Post by vilhelm_s »

wging wrote: post #82
vilhelm_s wrote: post #79

Earlier quoted context omitted.

Agreed in general, but it is possible to enable this style of constraint propagation by being restrictive about what kind of contraints you can write. In particular, the "LIQUID" family of languanges that have been developed at UCSD allows properties which are conjunctions of LInear IneQUlites, and can infer them automatically. The programmer would annotate one declaration of a variable with a constraint like (0 Thei…

http://goto.ucsd.edu:8090/index.html ?

Thanks!

Re: Programming paradigms that change how you think about coding

#98

Post by ExpiredLink »

sergiosgc wrote: post #96

Where is Aspect Oriented Programming and all the other offspring of the Inversion of Control pattern (Dependency Injection, Dependency Inversion, ...)? Is this line of evolution in languages considered dead?

Yes, thank heavens, yes!

Re: Programming paradigms that change how you think about coding

#99

Post by ExpiredLink »

bru wrote: post #3

Some notes: - parallel and concurrent are 2 different things - the 'symbolic languages' definition seems off. Wikipedia puts it right: > symbolic programming is computer programming in which the program can manipulate formulas and program components as data So it's not "using graphs & such to program"

@see http://www.reddit.com/r/programming/comments/22nhb2/six_prog...

for some valid critique.

Post reply on HN