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

121–130 of 206 posts

Re: Programming paradigms that change how you think about coding

#121

Post by AlexanderDhoore »

The aurora language seems very interesting. Too bad there is already another language called Aurora...

I makes me think of Elm [1] and (functional) reactive programming. Reactive programming is fantastic. It's kind of like how a spreadsheet program works. If a variable changes, all variables who depend on it change as well. Given "a = b + c", if c increments by 1, so does a.

It has many advantages over event based systems, like Javascript. Reactive programs don't need callbacks. The changing values propagate the "event" through the system.

I'd love to hear what you guys think about this direction of programming. It seems very natural to me.

Edit: I also see reactive programming as the golden way of having changing state in functional languages. Functional languages have no problem with data or state. They have a problem with change of state. The reactive paradigm solves that problem. All change is implicit and code can be exactly as functional as before.

[1] http://elm-lang.org/

[2] http://en.wikipedia.org/wiki/Reactive_programming

Re: Programming paradigms that change how you think about coding

#122

Post by platz »

sold wrote: post #91
JadeNB wrote: post #76

Earlier quoted context omitted.

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…

The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system.

I hear Idris is more reasonable in this regard and has better general purpose programming properties.

Re: Programming paradigms that change how you think about coding

#123

Post by dllthomas »

Kutta wrote: post #119
dllthomas wrote: post #115

Earlier quoted context omitted.

"You can always just refuse to run any function compile time that has not yet passed termination check." I don't understand this sentence.

Both Idris and Agda check whether functions provably terminate. Halting problem notwithstanding it is possible to have conservative checks that never return false positives, so that an OK from the checker implies termination, but a FAIL doesn't imply non-termination. Idris is not total by default, so it is not required that all functions pass the termination check. However, when Idris does the type checking it has to…

So that was "You can always just refuse to run any function [at] compile time that has not yet passed termination check."?

All of this is certainly the case, and useful, and interesting. It doesn't contradict the point that 1) guaranteeing termination and 2) guaranteeing you return "no" on every incorrectly typed program are incompatible, which was approximately the original question.

Re: Programming paradigms that change how you think about coding

#124

Post by ibdknox »

AlexanderDhoore wrote: post #121

The aurora language seems very interesting. Too bad there is already another language called Aurora... I makes me think of Elm [1] and (functional) reactive programming. Reactive programming is fantastic. It's kind of like how a spreadsheet program works. If a variable changes, all variables who depend on it change as well. Given "a = b + c", if c increments by 1, so does a. It has many advantages over event based sy…

we're actually in the process of changing the name :)

EDIT: re FRP, you might find this Lambda The Ultimate post insightful: http://lambda-the-ultimate.org/node/4900

FRP has issues with openness and isn't real great at dealing with collections. It also forces you to express things kind of unnaturally (e.g. instead of "click this and increment x", you say "the counter is the count of all click events"). There are other methods of managing time, like Glitch[1] and Bloom[2] that seem more promising :)

[1]: http://lambda-the-ultimate.org/node/4910 [2]: http://boom.cs.berkeley.edu/

Re: Programming paradigms that change how you think about coding

#125

Post by solomatov »

arjunnarayan wrote: post #93
jarrett wrote: post #87

Earlier quoted context omitted.

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.

>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.

In dependently typed programming languages like agda and Idris typechecking is decidable. You are wrong here.

Re: Programming paradigms that change how you think about coding

#126

Post by brikis98 »

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"

Thanks for the feedback. I updated the post with notes that mention these corrections.

Re: Programming paradigms that change how you think about coding

#127

Post by solomatov »

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…

>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.

They don't prove theorems. You do this by writing a program.

Re: Programming paradigms that change how you think about coding

#128

Post by [deleted] »

ibdknox wrote: post #124
AlexanderDhoore wrote: post #121

The aurora language seems very interesting. Too bad there is already another language called Aurora... I makes me think of Elm [1] and (functional) reactive programming. Reactive programming is fantastic. It's kind of like how a spreadsheet program works. If a variable changes, all variables who depend on it change as well. Given "a = b + c", if c increments by 1, so does a. It has many advantages over event based sy…

we're actually in the process of changing the name :) EDIT: re FRP, you might find this Lambda The Ultimate post insightful: http://lambda-the-ultimate.org/node/4900 FRP has issues with openness and isn't real great at dealing with collections. It also forces you to express things kind of unnaturally (e.g. instead of "click this and increment x", you say "the counter is the count of all click events"). There are othe…

[deleted]

Re: Programming paradigms that change how you think about coding

#129

Post by solomatov »

platz wrote: post #122
sold wrote: post #91

Earlier quoted context omitted.

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…

The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system. I hear Idris is more reasonable in this regard and has better general purpose programming properties.

>The problem with theorem provers like Adga and Coq is they are brittle to refactoring and thus hard to make changes to an app. Something seeming small can ripple through the whole system. I hear Idris is more reasonable in this regard and has better general purpose programming properties.

You can say the same for any strongly typed language, but reality is it's the opposite. If your program has a good design, it's easy to refactor.

Re: Programming paradigms that change how you think about coding

#130

Post by AlexanderDhoore »

ibdknox wrote: post #124
AlexanderDhoore wrote: post #121

The aurora language seems very interesting. Too bad there is already another language called Aurora... I makes me think of Elm [1] and (functional) reactive programming. Reactive programming is fantastic. It's kind of like how a spreadsheet program works. If a variable changes, all variables who depend on it change as well. Given "a = b + c", if c increments by 1, so does a. It has many advantages over event based sy…

we're actually in the process of changing the name :) EDIT: re FRP, you might find this Lambda The Ultimate post insightful: http://lambda-the-ultimate.org/node/4900 FRP has issues with openness and isn't real great at dealing with collections. It also forces you to express things kind of unnaturally (e.g. instead of "click this and increment x", you say "the counter is the count of all click events"). There are othe…

Well, I'm not a fan of the "use folds over time" concept either. FRP is too complex, but there's some great ideas there.

Would you say Aurora and these other languages are "reactive"? Or do you have a better term for it?

BTW: I'm reading "Toward a better programming" right now :)

Post reply on HN