Correctness – A paradigm for sustainable software development • Hacker News Board

Re: Correctness – A paradigm for sustainable software development

#171

Post by mpweiher » Sun, Apr 07, 2019, 10:29 AM UTC

sevensor wrote: post #81

pron wrote: post #79

As someone who practices and encourages others to employ formal methods in software development, I'm disappointed to read a post that claims FP has some significant effect on correctness. This has not been established, and does not at all appear to be the case. There are many aspects, including techniques and tools, that can positively affect program correctness. The choice of a programming language or even a paradig…

There are certainly a lot of people who feel that way, though. Especially when the language has an expressive type system. Would you say these languages merely swap one kind of error for another?

> who feel that way

You hit the nail on the head:

The Safyness of Static Typing

https://blog.metaobject.com/2014/06/the-safyness-of-static-t...

(This is obviously for static typing, not FP, but the mechanism appears largely the same and the overlap is substantial)

Re: Correctness – A paradigm for sustainable software development

#172

Post by specialist » Sun, Apr 07, 2019, 5:54 PM UTC

agentultra wrote: post #39

specialist wrote: post #28

Earlier quoted context omitted.

"...but the real problem is the mountain." Terrific metaphor, thank you. I've been stuck with "the map is not the territory" for ages, which is too meta for polite convo. With "maps / territory", I never thought to ask "do we have to summit the mountain? can we take the valley, the pass? can we tunnel? go around?" "Grumpy programmers who think maths is for academics are going to miss out" Probably. I'm still stuck ea…

The original thread: https://twitter.com/pressron/status/1109974207243390977 Where I chimed in: https://twitter.com/agentultra/status/1112752548656660482

Belated thanks. I like the additional expressive power of considering the terrain, eg rocky vs smooth.

Re: Correctness – A paradigm for sustainable software development

#173

Post by newacctjhro » Mon, Apr 08, 2019, 4:37 AM UTC

tombert wrote: post #3

chalst wrote: post #2

I hope this article strikes a chord. Two quibbles: Haskell is prone to something that might be considered a class of bug that Rust avoid: the space and time performance of idiomatic Haskell code can be very surprising. I also wonder at the possible answers you give to " “When” would you say that the software had a bug?" - the most obvious answer to me is when the commit is made to the codebase that introduces possibl…

I think it's experimental right now, but Idris (which I consider the "Child of Haskell"), has basic support for linear types [1], which could at least help the space-prediction problems. Doesn't hurt that Idris isn't lazy-by-default either. My point is that I actually think that Idris could end up being successful in an industrial sense, due to the fact that it gives you all the correctness guarantees of Haskell (and…

This stuff feels like a proof of concept that isn't really integrated to the rest of the language (Kinda like OCaml's OO). For example, it's unfortunate that Type, UniqueType and BorrowedType are different kinds (in Rust, they are the same kind; stuff that isn't "unique" just implement Copy)

Rust's advantage is that its borrow system, with reborrowing rules and such, feels much more ergonomic.

Re: Correctness – A paradigm for sustainable software development

#174

Post by tombert » Mon, Apr 08, 2019, 2:31 PM UTC

newacctjhro wrote: post #173

tombert wrote: post #3

Earlier quoted context omitted.

I think it's experimental right now, but Idris (which I consider the "Child of Haskell"), has basic support for linear types [1], which could at least help the space-prediction problems. Doesn't hurt that Idris isn't lazy-by-default either. My point is that I actually think that Idris could end up being successful in an industrial sense, due to the fact that it gives you all the correctness guarantees of Haskell (and…

This stuff feels like a proof of concept that isn't really integrated to the rest of the language (Kinda like OCaml's OO). For example, it's unfortunate that Type, UniqueType and BorrowedType are different kinds (in Rust, they are the same kind; stuff that isn't "unique" just implement Copy) Rust's advantage is that its borrow system, with reborrowing rules and such, feels much more ergonomic.

You're not wrong, but the fact that some work is being done on this is at least a good sign I think. A proof-of-concept is necessary before you can integrate these things organically into the language, and I that as a result it could be pretty interesting.

If I knew anything about elaborate type systems, I would try and address your complaints. Sadly, my knowledge of linear logic and whatnot is very ad hoc.

Re: Correctness – A paradigm for sustainable software development

#175

Post by agentultra » Mon, Apr 08, 2019, 3:29 PM UTC

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…

This is way off topic but how far did you get with Haskell? I was a Python programmer, contributor, and speaker for ~10 years and felt I was way more productive in it than in Haskell -- but after spending the last few years with Haskell I now find the opposite to be true and hardly write Python anymore.

Haskell let's me encode more of the business logic at the type level. I've finally been able to experience what people mean when they say a type system as good as Haskell's allow you to make sure invalid states are not presentable.

I can do the same in Python, Javascript, etc but it's much more work by writing thousands of lines of test code and still not being certain where the edge cases are.

That's one area a rich type system helps with...

but I think more to the spirit of your comment: it's the behaviors that are most important. No language is sufficiently expressive enough to define what those behaviors should be, and more importantly, which behaviors are not allowed. I totally agree that whether Haskell or Python, when it comes to this problem, neither are effective! There are no compile-time or run-time errors and yet we observe incorrect behavior! That's something I've only seen formal methods able to tackle.

Re: Correctness – A paradigm for sustainable software development

#176

Post by mlthoughts2018 » Mon, Apr 08, 2019, 5:18 PM UTC

agentultra wrote: post #175

mlthoughts2018 wrote: post #162

Earlier quoted context omitted.

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…

This is way off topic but how far did you get with Haskell? I was a Python programmer, contributor, and speaker for ~10 years and felt I was way more productive in it than in Haskell -- but after spending the last few years with Haskell I now find the opposite to be true and hardly write Python anymore. Haskell let's me encode more of the business logic at the type level. I've finally been able to experience what peo…

I spent about 4 years total working professionally in Haskell, commonly using things like multi-parameter type classes, liquidhaskell, compiler extensions for fully dependent types, higher kinded types.

I’ve heard the claim, “Haskell let me encode business logic into the type system” so many times, but I think it’s totally a false promise. Usually people mean design patterns like phantom types and things, and it just leads to the same spaghetti code messes as in any other paradigm.

I’ve never found any cases where encoding this stuff into the type system actually resulted in verifiably more correct code as compared to doing the same thing with analogous patterns in dynamic typing languages and adding lightweight tests. You still end up needing approximately the same amount of test code either way.

Yet in the statically typed case, you often pay a big constant penalty of compile time overhead delaying the work cycle, even for the best incremental compilers.

Re: Correctness – A paradigm for sustainable software development

#177

Post by int_19h » Mon, Apr 08, 2019, 8:53 PM UTC

naasking wrote: post #169

int_19h wrote: post #138

Earlier quoted context omitted.

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.

> Encapsulation is a core principle of OOP.

That's exactly the assertion that I'd like substantiated. I don't think there's consensus on this. Sure, it's mentioned in the oft-cited "encapsulation, inheritance, polymorphism, abstraction" mantra - but so is inheritance, and yet prototype-based OO doesn't have it.

Personally, I would say that the only core principles of OOP are object identity (i.e. objects are distinguishable aside from their state), and polymorphism via dynamic dispatch. Everything else is optional.

Re: Correctness – A paradigm for sustainable software development

#178

Post by wellpast » Tue, Apr 09, 2019, 2:54 AM UTC

demilicious wrote: post #140

wellpast wrote: post #100

> what is the language and mindset of “objects” with dynamic dispatch providing you apart from an endless stream of bugs that seem to keep reoccurring everytime you try an evolve the software to introduce a new requirement? The only mindset required to avoid long-term bugs and maintenance problems is a personal conscientiousness, a personal approach to defensive programming based on (ideally, extensive) personal expe…

This makes a whole lot of sense to me. However, one of the elements of truly productive learning is _focused_ practice; that is, practice with mindfulness and intentionality directed at a specific element. One won't necessarily get any better at decoupling unless it is specifically practiced. To that end, _how_ would one truly practice the skill of decoupling? Or maybe, what resources or heuristics or strategies woul…

I think you're hitting the nail on the head. It is specific and focused practice. I've been thinking about working on a book or set of blog posts or something to try to flesh out what a regimen would look like.

Most writing on software of course is technical (on PLs, algorithms, processes) but there seems to be very little to guide the software practitioner who really wants to seek mastery.

> what resources or heuristics or strategies would you suggest to help draw the lines between behaviours or modules?

The best I can come up with for teaching this would be to create some concrete "problems"/scenarios that would exercise the skill set, and then reveal various ways the problem could be decomposed and quantify the degree of decoupling and even reveal the practical consequence of the coupling by introducing new "requirements"/dimensions to the scenario.

Re: Correctness – A paradigm for sustainable software development

#179

Post by [deleted] » Tue, Apr 09, 2019, 10:49 AM UTC

mlthoughts2018 wrote: post #176

agentultra wrote: post #175

Earlier quoted context omitted.

This is way off topic but how far did you get with Haskell? I was a Python programmer, contributor, and speaker for ~10 years and felt I was way more productive in it than in Haskell -- but after spending the last few years with Haskell I now find the opposite to be true and hardly write Python anymore. Haskell let's me encode more of the business logic at the type level. I've finally been able to experience what peo…

I spent about 4 years total working professionally in Haskell, commonly using things like multi-parameter type classes, liquidhaskell, compiler extensions for fully dependent types, higher kinded types. I’ve heard the claim, “Haskell let me encode business logic into the type system” so many times, but I think it’s totally a false promise. Usually people mean design patterns like phantom types and things, and it just…

[deleted]

Re: Correctness – A paradigm for sustainable software development

#180

Post by naasking » Tue, Apr 09, 2019, 12:52 PM UTC

int_19h wrote: post #177

naasking wrote: post #169

Earlier quoted context omitted.

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.

> Encapsulation is a core principle of OOP. That's exactly the assertion that I'd like substantiated. I don't think there's consensus on this. Sure, it's mentioned in the oft-cited "encapsulation, inheritance, polymorphism, abstraction" mantra - but so is inheritance, and yet prototype-based OO doesn't have it. Personally, I would say that the only core principles of OOP are object identity (i.e. objects are distingu…

There's a historical argument: encapsulation was in Cardelli's original object calculi, and part of every OO language of the time.

There's also a conceptual argument: dynamic dispatch and object identity both require encapsulation. What do you think you're dispatching or comparing equality on if not hidden state?