6 ms·

I had a thread on twitter about this problem of "musicians nerding over gear." In our metaphor it was about mountain climbers. The programming language and its

I had a thread on twitter about this problem of "musicians nerding over gear." In our metaphor it was about mountain climbers. The programming language and its paradigms chosen may have some effect on how you scale the mountain but the real problem is the mountain. Whether you use functional programming or dynamic typing it only affects small, local problems in the practice of climbing mountains. The problem of efficiently scaling mountains requires a broader scope. This is why I think formal methods are starting to break into the mainstream: they give us tools to use to simulate and verify designs (model checking, system design validation), validate implementations (verification, proof), and generate provably correct code from high level specifications (synthesis). Grumpy programmers who think maths is for academics are going to miss out I think. It's an exciting field and the cost for something that used to be only used for extreme circumstances has been coming down so rapidly that it can be effectively used in small businesses as well. It all comes down to clarity: in communication, in thought, and in practice.

gtirloni 8y ago
Amy pointers to documentation that's approachable by beginners?
- agentultra 8y ago
  https://www.youtube.com/watch?v=hhGnMbw98u8 https://www.youtube.com/watch?v=hhGnMbw98u8 https://www.youtube.com/watch?v=tfnldxWlOhM https://www.youtube.com/watch?v=tfnldxWlOhM https://www.youtube.com/watch?v=HnOix9TFy1A https://www.youtube.com/watch?v=HnOix9TFy1A https://pron.github.io/posts/tlaplus-curryon-talk https://pron.github.io/posts/tlaplus-curryon-talk https://learntla.com/introduction/ https://learntla.com/introduction/ https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/ https://rise4fun.com/dafny https://rise4fun.com/dafny
- nickpsecurity 8y ago
  Check out the Alloy model checker. Simple with GUI, too. One guy I know says he just uses it like SQL. Hillel Wayne just published Practical TLA+. It helps with concurrency and distributed systems. There's the book on SPARK Ada which lets you do system code that's provably safe. Finally, the easiest method to use in any language is Design-by-Contract. https://www.betterworldbooks.com/product/detail/Practical-TLA---Planning-Driven-Development-9781484238288 https://www.betterworldbooks.com/product/detail/Practical-TL... https://www.betterworldbooks.com/product/detail/Building-High-Integrity-Applications-with-SPARK-9781107656840 https://www.betterworldbooks.com/product/detail/Building-Hig... https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/
  - agentultra 8y ago
    I recently started using Alloy for small models. Great for searching for constraints and state machines.
specialist 8y ago
"...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 eating the paste, banging the rocks together. Still arguing that Chain of Command is not nested Decorators, trying to explain that memcached (or redis) in parallel vs write thru is a replicant and not a cache, that "agile velocity" means spunk if you're not tracking your defect rate, that Spring & J2EE style DI & IoC is dynamic programming envy (just use Python), etc. "It all comes down to clarity..." God help us. PS- Reading that Twitter thread might be fun, if you have a link handy.
- agentultra 8y ago
  The original thread: https://twitter.com/pressron/status/1109974207243390977 https://twitter.com/pressron/status/1109974207243390977 Where I chimed in: https://twitter.com/agentultra/status/1112752548656660482 https://twitter.com/agentultra/status/1112752548656660482
  - specialist 8y ago
    Belated thanks. I like the additional expressive power of considering the terrain, eg rocky vs smooth.
l_t 8y ago
Interesting point. I think I've been feeling this lately as a desire to have, basically, smarter compilers. It's actually incredible to me when I think about how many minutes of human thought are wasted among myself and my peers to informally verify facts about our programs. Obviously, types and tests help. But it's astonishing how much incidental complexity creeps into one's everyday work with our current tools. Under most circumstances telling a computer to do something shouldn't be that much harder than telling a human to do it (assuming a concrete grammar and shared vocabulary).
- dhimes 8y ago
  I find it helpful to think of it as teaching a computer to do something rather than telling it to.
- mlthoughts2018 8y ago
  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 if you get your program to compile, it’s very likely to be correct and run without error. I’ve emphatically never found that to be true. The types of bugs that compilers can help with are very simplistic most of the time. Requesting a method or attribute that doesn’t exist, typos, confusion about arguments passed to a function. In dynamic typing, you also solve these same things in a super cheap and low effort way with unit tests. Additional behavioral unit tests are where real effort becomes required, and these are needed in any paradigm. Compilers are also not free. My experience with the Scala compiler for example was awful. It is so incredibly slow to compile that I absolutely would rather give up type checking and just use some cheap unit tests to have a much faster development cycle. When you make 1 or 2 small changes and even a smart incremental compiler setup like zinc needs to recompile 30 code units and it takes ~ 3 minutes before you can run tests, this is maddening, and the cycle repeats the whole time you’re working, so it’s this constant extremely disruptive expense. I’ve had similar thinga happen in legacy code bases with Haskell too.
aeorgnoieang 8y ago
One problem with your metaphor about mountain climbers and mountain climbing is that the most efficient way to scale a mountain is probably to just take a helicopter to the top. Mountain climbing, like lots of other things, _must_ be constrained, in some way, to be _meaningful_, and the constraints _chosen_ reflect the _purpose_ of the endeavor. But then, specific constraints, e.g. the tools and methods 'allowed', become their own 'thing' (while continuing to interact with and evolve with other related things).
- agentultra 8y ago
  It's an analogy. There are holes in every analogy. The image I was trying to invoke and the idea implied was that programming languages are insufficiently expressive enough on their own to solve the hard problems in designing systems. They lack the ability to reason abstractly about other processes, agents, and shared state such that they cannot prove anything about their behavior in the context of a larger system. They can't express invariants about the complicated universe of possible behaviors. And the kinds of problems we're tackling today are built on large systems: several interacting processes over an unreliable network working in concert across the globe to keep your data consistent and always available: that's the mountain. Arguing about which programming language or paradigm to use has only a small part to play in the solution to the problem.
- UnFleshedOne 8y ago
  Metaphor survives if you then say that to take helicopter to the top you need to build a helicopter first and learn how to pilot it in mountain conditions. Suddenly taking an ice pick and just going up sounds simpler.
  - dope99 8y ago
    Ah, so you are referring to Haskell.
ummonk 8y ago
Formal methods are to programming like ropes are to mountain climbing. >Whether you use functional programming or dynamic typing it only affects small, local problems in the practice of climbing mountains. Static typing is a type of formal method.
- tsimionescu 8y ago
  Yes, but the range of what 'static typing' means is so large that it is meaningless in this case. C is statically typed, and so are Java and OCaml. So is Idris. Of these, only Idris' type system has any power to model truly interesting properties (though the cost of doing so, in program complexity, is huge). Otherwise, even something as simple as rejecting `add(x, y) return x - y;` as a well typed function is beyond all of the others.
  - ummonk 8y ago
    Formal systems obviously differ in their verification power and ease of use. E.g. with type systems, in terms of power on one end you have unsound type systems and on the other end you have dependent types. Sound type systems with algebraic data types tend to be quite common though and reasonably powerful. As far as ease of use goes, type inference and flow analysis goes a very long way. >Otherwise, even something as simple as rejecting `add(x, y) return x - y;` as a well typed function is beyond all of the others. Why shouldn’t that be well typed (unless it is invoked with unsuitable argument types)? Are you saying the language should magically understand the english language meaning of “add”?
    - deleted 8y ago
      [deleted]
    - tsimionescu 8y ago
      No, I'm saying that there is no way to encode even such a simple property as 'addition of two numbers produces a bigger number' in the type systems of most languages out there (including stuff like the ML family), which is probably why (non-dpendent/linear/other advanced) type systems have never been shown to improve program correctness the way other formal techniques have. Even simple type systems help in other ways (ease of development, documentation, performance).
pron 8y ago
When I made that comparison I meant to highlight the fact that physics determines a certain minimal amount of work required to raise a body of a certain mass to the top of the mountain. Any improvements in efficiency is small in comparison to that required work. So that is the first thing we must understand: there is a large cost to building something complex, and nothing can drastically reduce it. Formal methods -- or any other useful technique -- are beneficial only once you understand this. Most of the cost is determined by what you build, not how you build it, so the only way to drastically cut it is to build drastically less. Once you've decided what it is that you need to build, you must be ready to pay the cost.

gtirloni 8y ago

Amy pointers to documentation that's approachable by beginners?

agentultra 8y ago
https://www.youtube.com/watch?v=hhGnMbw98u8 https://www.youtube.com/watch?v=hhGnMbw98u8 https://www.youtube.com/watch?v=tfnldxWlOhM https://www.youtube.com/watch?v=tfnldxWlOhM https://www.youtube.com/watch?v=HnOix9TFy1A https://www.youtube.com/watch?v=HnOix9TFy1A https://pron.github.io/posts/tlaplus-curryon-talk https://pron.github.io/posts/tlaplus-curryon-talk https://learntla.com/introduction/ https://learntla.com/introduction/ https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/ https://rise4fun.com/dafny https://rise4fun.com/dafny
nickpsecurity 8y ago
Check out the Alloy model checker. Simple with GUI, too. One guy I know says he just uses it like SQL. Hillel Wayne just published Practical TLA+. It helps with concurrency and distributed systems. There's the book on SPARK Ada which lets you do system code that's provably safe. Finally, the easiest method to use in any language is Design-by-Contract. https://www.betterworldbooks.com/product/detail/Practical-TLA---Planning-Driven-Development-9781484238288 https://www.betterworldbooks.com/product/detail/Practical-TL... https://www.betterworldbooks.com/product/detail/Building-High-Integrity-Applications-with-SPARK-9781107656840 https://www.betterworldbooks.com/product/detail/Building-Hig... https://hillelwayne.com/post/pbt-contracts/ https://hillelwayne.com/post/pbt-contracts/
- agentultra 8y ago
  I recently started using Alloy for small models. Great for searching for constraints and state machines.

specialist 8y ago

"...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 eating the paste, banging the rocks together. Still arguing that Chain of Command is not nested Decorators, trying to explain that memcached (or redis) in parallel vs write thru is a replicant and not a cache, that "agile velocity" means spunk if you're not tracking your defect rate, that Spring & J2EE style DI & IoC is dynamic programming envy (just use Python), etc. "It all comes down to clarity..." God help us. PS- Reading that Twitter thread might be fun, if you have a link handy.

agentultra 8y ago
The original thread: https://twitter.com/pressron/status/1109974207243390977 https://twitter.com/pressron/status/1109974207243390977 Where I chimed in: https://twitter.com/agentultra/status/1112752548656660482 https://twitter.com/agentultra/status/1112752548656660482
- specialist 8y ago
  Belated thanks. I like the additional expressive power of considering the terrain, eg rocky vs smooth.

l_t 8y ago

Interesting point. I think I've been feeling this lately as a desire to have, basically, smarter compilers. It's actually incredible to me when I think about how many minutes of human thought are wasted among myself and my peers to informally verify facts about our programs. Obviously, types and tests help. But it's astonishing how much incidental complexity creeps into one's everyday work with our current tools. Under most circumstances telling a computer to do something shouldn't be that much harder than telling a human to do it (assuming a concrete grammar and shared vocabulary).

dhimes 8y ago
I find it helpful to think of it as teaching a computer to do something rather than telling it to.
mlthoughts2018 8y ago
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 if you get your program to compile, it’s very likely to be correct and run without error. I’ve emphatically never found that to be true. The types of bugs that compilers can help with are very simplistic most of the time. Requesting a method or attribute that doesn’t exist, typos, confusion about arguments passed to a function. In dynamic typing, you also solve these same things in a super cheap and low effort way with unit tests. Additional behavioral unit tests are where real effort becomes required, and these are needed in any paradigm. Compilers are also not free. My experience with the Scala compiler for example was awful. It is so incredibly slow to compile that I absolutely would rather give up type checking and just use some cheap unit tests to have a much faster development cycle. When you make 1 or 2 small changes and even a smart incremental compiler setup like zinc needs to recompile 30 code units and it takes ~ 3 minutes before you can run tests, this is maddening, and the cycle repeats the whole time you’re working, so it’s this constant extremely disruptive expense. I’ve had similar thinga happen in legacy code bases with Haskell too.

aeorgnoieang 8y ago

One problem with your metaphor about mountain climbers and mountain climbing is that the most efficient way to scale a mountain is probably to just take a helicopter to the top. Mountain climbing, like lots of other things, _must_ be constrained, in some way, to be _meaningful_, and the constraints _chosen_ reflect the _purpose_ of the endeavor. But then, specific constraints, e.g. the tools and methods 'allowed', become their own 'thing' (while continuing to interact with and evolve with other related things).

agentultra 8y ago
It's an analogy. There are holes in every analogy. The image I was trying to invoke and the idea implied was that programming languages are insufficiently expressive enough on their own to solve the hard problems in designing systems. They lack the ability to reason abstractly about other processes, agents, and shared state such that they cannot prove anything about their behavior in the context of a larger system. They can't express invariants about the complicated universe of possible behaviors. And the kinds of problems we're tackling today are built on large systems: several interacting processes over an unreliable network working in concert across the globe to keep your data consistent and always available: that's the mountain. Arguing about which programming language or paradigm to use has only a small part to play in the solution to the problem.
UnFleshedOne 8y ago
Metaphor survives if you then say that to take helicopter to the top you need to build a helicopter first and learn how to pilot it in mountain conditions. Suddenly taking an ice pick and just going up sounds simpler.
- dope99 8y ago
  Ah, so you are referring to Haskell.

ummonk 8y ago

Formal methods are to programming like ropes are to mountain climbing. >Whether you use functional programming or dynamic typing it only affects small, local problems in the practice of climbing mountains. Static typing is a type of formal method.

tsimionescu 8y ago
Yes, but the range of what 'static typing' means is so large that it is meaningless in this case. C is statically typed, and so are Java and OCaml. So is Idris. Of these, only Idris' type system has any power to model truly interesting properties (though the cost of doing so, in program complexity, is huge). Otherwise, even something as simple as rejecting `add(x, y) return x - y;` as a well typed function is beyond all of the others.
- ummonk 8y ago
  Formal systems obviously differ in their verification power and ease of use. E.g. with type systems, in terms of power on one end you have unsound type systems and on the other end you have dependent types. Sound type systems with algebraic data types tend to be quite common though and reasonably powerful. As far as ease of use goes, type inference and flow analysis goes a very long way. >Otherwise, even something as simple as rejecting `add(x, y) return x - y;` as a well typed function is beyond all of the others. Why shouldn’t that be well typed (unless it is invoked with unsuitable argument types)? Are you saying the language should magically understand the english language meaning of “add”?
  - deleted 8y ago
    [deleted]
  - tsimionescu 8y ago
    No, I'm saying that there is no way to encode even such a simple property as 'addition of two numbers produces a bigger number' in the type systems of most languages out there (including stuff like the ML family), which is probably why (non-dpendent/linear/other advanced) type systems have never been shown to improve program correctness the way other formal techniques have. Even simple type systems help in other ways (ease of development, documentation, performance).

pron 8y ago

When I made that comparison I meant to highlight the fact that physics determines a certain minimal amount of work required to raise a body of a certain mass to the top of the mountain. Any improvements in efficiency is small in comparison to that required work. So that is the first thing we must understand: there is a large cost to building something complex, and nothing can drastically reduce it. Formal methods -- or any other useful technique -- are beneficial only once you understand this. Most of the cost is determined by what you build, not how you build it, so the only way to drastically cut it is to build drastically less. Once you've decided what it is that you need to build, you must be ready to pay the cost.