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

Correctness – A paradigm for sustainable software development

nonullpointers.com

Post reply on HN
Print view View original

161–170 of 186 posts

Re: Correctness – A paradigm for sustainable software development

#161

Post by pron »

cannabis_sam wrote: post #160
pron wrote: post #156

Earlier quoted context omitted.

1. When did I mention types? I was talking about FP vs imperative. There are typed and untyped languages in both paradigms. There actually have been a couple of studies that found a positive effect for types on correctness. The largest effect (15%!) was reported in this paper: http://earlbarr.com/publications/typestudy.pdf but it compared only TypeScript and JavaScript. 2. Why the different category? Both effects wer…

1. Here: https://news.ycombinator.com/item?id=19586915 > Explaining why it is unlikely (from a theory perspective) that languages like Haskell have a significant effect on correctness is easier [2] > It's relatively easy to classify which program properties can be assisted by the language and which cannot. Those that can (e.g. memory safety and type safety) are called inductive (or compositional). They can be helpful…

I mentioned type safety in passing, but I wasn't talking about the effect of types on correctness in this discussion. That's a more nuanced one.

> your are conflating the question " could (typed) FP be use for correctness" with " should (typed) FP be use for correctness", and while the answer to the first one is trivially "yes", you appear to be chasing the answer you want ("no") to the second question.

I am not conflating anything, and I certainly didn't say which programming paradigm people should or shouldn't use. I did say that if people care about correctness, they should look elsewhere than to change their preferred paradigm to or from FP, and focus on techniques that seem to have an actual effect on correctness (BTW, switching languages -- among several reasonable choices -- is often costly, and language in general is one of the choices with the least drastic effect on most important software metrics, except maybe when it comes to performance, where most of the time what matters is the runtime, and not so much the programming paradigm).

BTW, while I won't get into the discussion about types (which, again, is complicated, as there are different kind of types and usage of types, each with very different cost/benefit), the largest effect types -- and language choice in general -- have on correctness was found in a study I linked in another comment to be of 15% (in bug reduction), when comparing TypeScript and JavaScript. In contrast, several studies and case studies have found code reviews to have an average effect of ~60%. So the largest effect language choice was ever found to have in a single study is 4x smaller than the effect of techniques that are far cheaper than a language change (well, maybe not in the case of TypeScript/JavaScript). Really, language is one of the costliest and least impactful factors on correctness (except maybe when the language is unsafe).

In summary, no connection between FP and correctness has been established, period (and what little evidence we have seems to suggest there is none). People should use whatever paradigm/language they like; the chosen paradigm doesn't seem to have a large positive or a negative effect on correctness. People shouldn't make empirical claims that are unsubstantiated.

> Because homeopathy's claims and method of action can be dismissed a priori, due to the fact that they don't follow the laws of nature or the chemical principles of solvation.

I wasn't trying to say that people who believe FP has an effect on correctness are exactly the same as those who believe in the effectiveness of homeopathy. I only said that the fact that some people make the claim enthusiastically in blog posts should not be taken as corroboration to its validity, just as the number of enthusiastic posts about homeopathy is not evidence in its favor. People often enthusiastically believe things that aren't true because personal experience can be misleading.

But anyway, the claim that FP improves correctness similarly does not follow any law of software correctness. If either homeopathy or FP were to have an effect, it would have to be through some as-of-yet undiscovered process. As any program could be mechanically translated between pure-FP and imperative, there is simply no CS theory to explain why FP would have an effect on correctness (as opposed to, say, using a model checker), and there is no such programming-process theory, either (as opposed to, say, code reviews).

Re: Correctness – A paradigm for sustainable software development

#162

Post by mlthoughts2018 »

ghettoimp wrote: post #130
dope99 wrote: post #125

Earlier quoted context omitted.

I’m not arguing here but honestly don’t know: how can interpretation be faster than the checking step of compilation? Maybe code generation takes more time, but Rust has ‘cargo check’ which only typechecks. Parsing is basically a wash between compilation and interpretation. Dynamic types still need to be resolved for the tests to run. So why would interpretation be faster? I’m working through a compiler book and woul…

I think mlthoughts2018 may be saying that he finds the advantages of a good "read-edit-test loop" to be more valuable than a compiler that catches type errors? It is certainly valuable. A good REPL is completely fantastic for prototyping and debugging. Being able to change how your program works while it's still running and has all its data loaded is great compared to a classic edit-compile-run cycle where you've got…

You are close to describing what I meant, except what I was saying is not related to a REPL.

For example, I find I am much more productive writing Python code instead of Scala or Haskell, after many years of experience in all three. By “productive” I mean writing fewer defects, completing programs more quickly, and validating that programs are sufficiently correct & efficient for deployment.

A typical work cycle in all 3 languages would be to read code, edit code, invoke a test command from a shell prompt (which triggers incremental re-compilation with Scala and Haskell). In business settings, even for very minor code changes, the incremental re-compilation would take on the order of a few minutes every time, and this was in large companies with sophisticated monorepo tooling and dedicated teams of tooling engineers who worked on performance for incremental compulation. For Python, I just run tests and get immediate feedback without waiting ~3 minutes every time.

The types of correctness verification offered by using the compiled languages and waiting ~3 minutes every cycle was just not useful. I got the same verification in Python by just writing some low effort extra tests one time and then save ~3 minutes on every edit-test cycle.

Re: Correctness – A paradigm for sustainable software development

#163

Post by cannabis_sam »

pron wrote: post #161
cannabis_sam wrote: post #160

Earlier quoted context omitted.

1. Here: https://news.ycombinator.com/item?id=19586915 > Explaining why it is unlikely (from a theory perspective) that languages like Haskell have a significant effect on correctness is easier [2] > It's relatively easy to classify which program properties can be assisted by the language and which cannot. Those that can (e.g. memory safety and type safety) are called inductive (or compositional). They can be helpful…

I mentioned type safety in passing, but I wasn't talking about the effect of types on correctness in this discussion. That's a more nuanced one. > your are conflating the question " could (typed) FP be use for correctness" with " should (typed) FP be use for correctness", and while the answer to the first one is trivially "yes", you appear to be chasing the answer you want ("no") to the second question. I am not conf…

>I mentioned type safety in passing

Thank you, that's what I meant.

> The claim that FP improves correctness similarly does not follow any law of software correctness. If either homeopathy or FP were to have an effect, it would have to be through some as-of-yet undiscovered process.

Again you are conflating could and should. Let's simplify:

Homeopathy CANNOT be used, since the concept fundamentally don't work and hence SHOULD not be used.

FP for correctness CAN be used, since we do have examples of functional languages that can be used with formal verification tools, type-based or otherwise. Whether it SHOULD be used, does not follow from whether it CAN/CANNOT be used. That's a question for the sociology of software engineering, and like you say, that's complex.

>People should use whatever paradigm/language they like

I agree, which is why I dislike when people try to associate certain preferences with pseudoscience.

Re: Correctness – A paradigm for sustainable software development

#164

Post by mlthoughts2018 »

int_19h wrote: post #142
mlthoughts2018 wrote: post #70

Earlier quoted context omitted.

I’ve programmed professionally in Haskell, Scala and Python in large projects across several jobs. In my experience, the compiler is rarely helpful at catching bugs. Most bugs, whether in a dynamic typing language or otherwise, are behavioral bugs that occur at runtime without generating explicit runtime errors, just incorrect but uninterrupted behavior. I always heard people make grandiose claims about Haskell, like…

> In dynamic typing, you also solve these same things in a super cheap and low effort way with unit tests. I wouldn't call it "super cheap and low effort", given that tests for stuff like "what if it's not an integer?" tend to be a large part of the overall unit test suite in dynamic languages. Just on the amount of code alone, I would say that it's far less effort to express that kind of stuff in types than in tests…

If you’re writing tests like “what if the input is not an integer” in Python, you’re probably doing a lot more stuff wrong. Dynamic typing is useful typically because you rarely need to check these types of issues. Instead you’d have some sort of input sanitizer that is responsible for all such inputs into a large system, and would include what type of failover logic should happen upon receiving a wrong input.

If you’re testing all kinds of different functions for argument checks or defensive programming conditions, it suggests a refactor to a central sanitizer pattern, and just one small set of sanitization tests. Other functions can take it for granted that the sanitizer works correctly.

You often need the same thing in statically typed systems anyway for cases when calculating whether an input is valid involves conditions not encoded by the type system (possibly even runtime configurable by the user). So except for all but the most trivial kinds of type validation, this does not actually constitute a difference in effort between the two paradigms anyway.

Re: Correctness – A paradigm for sustainable software development

#165

Post by BWStearns »

kaveh_h wrote: post #13

I started learning to write Haskell a while ago. My current reflection is while it’s easy to start learning to write simple code and correct code it a much larger step to actually be able to write performant code that is generic. Performant idiomatic Haskell requires a good enough understanding of the functional paradigm.

I experienced the same thing. Once you get over the practical application of monads hump it becomes a lot more like the progress experience in other languages. You don’t need to achieve your “monads are a burrito” moment to successfully write complex Haskell, you just need to be able to cargo cult while recognizing that you are doing so and the understanding will slowly accrete. That said, Haskell is the first language I’ve worked in where there are periodic learning cliffs (lenses stand out here) where when you scoot into a slightly foreign domain you need a few days of study. I still think the juice is worth the squeeze though since once you learn how to do the thing then doing the thing correctly tends to be easier in more forgiving languages.

Re: Correctness – A paradigm for sustainable software development

#166

Post by ghettoimp »

mlthoughts2018 wrote: post #162
ghettoimp wrote: post #130

Earlier quoted context omitted.

I think mlthoughts2018 may be saying that he finds the advantages of a good "read-edit-test loop" to be more valuable than a compiler that catches type errors? It is certainly valuable. A good REPL is completely fantastic for prototyping and debugging. Being able to change how your program works while it's still running and has all its data loaded is great compared to a classic edit-compile-run cycle where you've got…

You are close to describing what I meant, except what I was saying is not related to a REPL. For example, I find I am much more productive writing Python code instead of Scala or Haskell, after many years of experience in all three. By “productive” I mean writing fewer defects, completing programs more quickly, and validating that programs are sufficiently correct & efficient for deployment. A typical work cycle in a…

Thanks for the clarifications -- this is an interesting perspective.

For the last few years I think I've managed to land in the worst of both worlds with SystemVerilog. It manages to combine essentially no type system and no type checking (everything is implicitly just a bunch of bits) with abysmal compile times, so you get neither safety nor a quick turnaround.

All of this makes me really long for both a good type system, and a better edit-test cycle. Which is more valuable? You're probably right. There's nothing more frustrating than waiting 15 minutes to discover a missing comma...

Re: Correctness – A paradigm for sustainable software development

#167

Post by gambler »

int_19h wrote: post #141
Jtsummers wrote: post #48

Earlier quoted context omitted.

When viewed that way, you're not dealing with most mainstream OO languages anymore. But it is the intent of the originators of OO and I prefer the same view. Especially because at that point it becomes orthogonal to imperative/functional approaches. Message passing can be used with a functional language (Erlang) or an imperative language (Go) to great effect. It can also be added onto (as a library) most other langua…

It was the intent of Smalltalk, but not Simula, so it's not universal among the originators. Simula had actors implemented on top of objects and method calls, not the other way around. But in practice, does it really make that much difference? A method call is really just a synchronous message. So at that point we're really talking about what messages objects should have - and looking at something like String, Array…

>A method call is really just a synchronous message.

There is an important distinction. Messages are interpreted, at runtime. Which means you can do certain kinds of metaprogramming without getting outside of the normal tools of the language.

This is not a black-and-white kind of thing, though. A method call can be more or less like a message depending on the language tooling provided.

Re: Correctness – A paradigm for sustainable software development

#168

Post by int_19h »

gambler wrote: post #167
int_19h wrote: post #141

Earlier quoted context omitted.

It was the intent of Smalltalk, but not Simula, so it's not universal among the originators. Simula had actors implemented on top of objects and method calls, not the other way around. But in practice, does it really make that much difference? A method call is really just a synchronous message. So at that point we're really talking about what messages objects should have - and looking at something like String, Array…

>A method call is really just a synchronous message. There is an important distinction. Messages are interpreted, at runtime. Which means you can do certain kinds of metaprogramming without getting outside of the normal tools of the language. This is not a black-and-white kind of thing, though. A method call can be more or less like a message depending on the language tooling provided.

The tooling has also converged to some extent. Java is very much Simula-style, and methods calls aren't messages... except when they are:

https://www.baeldung.com/java-dynamic-proxies

C# also has something similar with TransparentProxy, not to mention "dynamic".

Re: Correctness – A paradigm for sustainable software development

#169

Post by naasking »

int_19h wrote: post #138
naasking wrote: post #113

Earlier quoted context omitted.

Yes, because those objects are a fusion of OOP and ADTs. Pure OOP does not permit violating procedural abstraction. To summarise, FP provides good reasoning in the small, and OO is needed in the large to orchestrate stateful services via protocols.

The paper that you're citing claims that "pure OOP" means "An object can only access other objects through their public interfaces". This feels like a very arbitrary definition to me, and one that does not correspond to what we deem OOP colloquially. Conversely, if the problem is "pure OOP", but most OOP that we actually use isn't "pure", then there's no problem.

Why is that arbitrary? Encapsulation is a core principle of OOP.

Re: there being no problem, that depends. Pure OOP has advantages and violating the properties often sacrifice some of those advantages.

Re: Correctness – A paradigm for sustainable software development

#170

Post by luord »

Yet another generic and sophomoric "the paradigms and type systems I prefer are so much better guise!" Piece.

This one is particularly obnoxious because he's aware of the tribalism and thinks that by mentioning it then his post is magically no longer merely more fuel to the decades-old flamewars.

Post reply on HN