Timeline for Non-OOP languages advantages and good uses
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 9, 2012 at 16:18 | vote | accept | Raphael | ||
| Dec 21, 2017 at 12:56 | |||||
| Dec 19, 2011 at 13:35 | comment | added | Raphael | And what about procedural programming? What are its advantages over other paradigms? | |
| Dec 17, 2011 at 17:23 | comment | added | SK-logic | @C.A.McCann, for a Turing-complete language, any type constraint just reads as "if an expression E returns a value, this value is of a type T". And the type system proves that all such constraints always holds - i.e., proves a "correctness". | |
| Dec 17, 2011 at 17:18 | comment | added | C. A. McCann | @SK-logic: A non-terminating expression can have any type, which constitutes a proof of every proposition, including false ones. It's hard to prove correctness when your proof system can't distinguish between "computes the desired result" and "gets stuck in an infinite loop"! From the Curry-Howard perspective, ML-inspired languages roughly translate to a logical system that includes "for all A, A is true" as an axiom. | |
| Dec 17, 2011 at 17:11 | comment | added | SK-logic | @C.A.McCann, a type system guarantees a proof that certain constraints always hold, and that's it, nothing more. Of course all the type systems are limited (but some of them guarantees a termination) - just as well as any other correctness proving techniques. Distinction between strict typing and proving correctness is quite vague, thanks to the Curry-Howard isomorphism. | |
| Dec 17, 2011 at 16:25 | comment | added | C. A. McCann | @SK-logic: Not in the presence of non-terminating expressions, which allow a program to "prove" anything. Look at the sort of answers I post on Stack Overflow--trust me, I'm very familiar with the distinction here. :] | |
| Dec 17, 2011 at 14:10 | comment | added | SK-logic | @C.A.McCann, en.wikipedia.org/wiki/Curry-Howard_correspondence - strict typing, seen in many functional languages, is somewhat equivalent to proving correctness. | |
| Dec 17, 2011 at 2:27 | comment | added | C. A. McCann | This doesn't really apply to any of the functional languages in practical use, though. There are languages designed for proving things which are based on functional programming, and can convert proofs to code in a functional language, but there's still a big difference between a proof in Coq and a program in OCaml. | |
| Dec 17, 2011 at 0:32 | comment | added | user4595 | Functions that have no side effect are also called pure functions. | |
| Dec 16, 2011 at 22:24 | history | answered | Dino | CC BY-SA 3.0 |