Hacker News Reader

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.

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.

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”?

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

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

I find it helpful to think of it as teaching a computer to do something rather than telling it to.

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.

I think most bugs are that kind that the compiler can catch. But yes absolutely a program can compile and be dead wrong. I’m writing a regex engine and lol at types saving me from all the mistakes I can make with building and transforming finite automata.

I’d still much rather have a slightly slow compilation than verify types in my head every time I’m in that area of code, or writing unit tests for every configuration of code which basically just validate I haven’t returned any nulls.

Typed compilation may take time, but it results in faster running programs. And unit tests also take time. I find the errors generated by a type checker come quicker and give more useful diagnostics for deep areas of the code.

My experience has been the opposite. Compilers are not just a little slow, but introduce a significant slowdown for every read-edit-test loop, which adds up to such huge productivity losses that any small gains from the compiler catching typo-style / wrong arguments sorts of bugs is totally erased.

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 would love to know.

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 to get your program's data re-loaded each time.

But I don't see that this has much to do with compilers versus interpreters, or even really dynamic versus static type checking...

- There are REPL-based environments with integrated compilers, and there are compiled languages with REPLs bolted on top.

- Good REPL support is surely more challenging for languages with strong static typing. After all: what does it mean to redefine a type? what happens to the functions that are using the old definitions? what happens to the instances of that type that are already alive in your program? But these problems all exist in dynamic languages too, it's just easy there to sweep them under the rug by treating them as yet more run-time errors.

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.

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

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.

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.

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

Well it's working for my code base so it's not a false promise.

I find it hard going back to dynamic languages now because of how little they allow you to see the types.

> I’ve never found any cases where encoding this stuff into the type system actually resulted in verifiably more correct code

I think there is still much debate about this. Dependent type theory is the only type system I know of in which it's possible to write proofs, and therefore verify, a program... but even dependent type theory alone is a bit bothersome for the task.

In my experience it's certainly possible to write a program in Python that is reasonably correct but it takes more effort.

Firstly, I didn’t mean to suggest you cannot write effective code in statically typed languages.. only that it is no easier and no more productive to do it than with dynamically typed languages.

> “In my experience it's certainly possible to write a program in Python that is reasonably correct but it takes more effort.”

I think there is a pivotal trade-off though. I’d argue that in many cases it can be less effort to write correct code in Python for three reasons,

- the simpler types of compiler checks are just inapplicable or handled by totally ignorably-low-effort unit tests in Python and don’t matter 99.9999% of the time, and have low cost in the 0.00001% of the time they do matter.

- the extra type system code and constraints it imposes introduces more extra code than what an analogous set of unit tests would have required for functionally the same level of correctness guarantee in Python.

- the extra time cost of including a compilation step in many edit cycle round trips adds up to far more effort than writing and maintaining extra tests, and disallows flexibly deciding when to get rapid feedback when that feedback matters more than whole-program correctness required by a compiler (and these points are magnified if ever working in a monorepo).

> 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 force your types to only ever interact with primitives at certain boundaries of your app, you can test for the "what if it's not an integer" stuff at the boundaries only. I.e. the core APIs never see a magic string, an integer, or any other such untyped thing.

In reality, there are always times where that falls a little flat, which is where IMO Gradual Typing comes into its own. The "core", with some assumptions about the boundaries, be statically analysed. You can add your times(int n) method safe in the knowledge that you'll get a runtime error if someone messes up the dynamic type or doesn't run the analyser.

Ultimately, as I want to run all my code before I put into to production, a lack of runtime errors from my tests tells me my code is correct for the situations I designed it to handle. Now if someone comes along later and manages to invoke a state that I hadn't considered, well... all bets are off.

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.

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

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.

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.

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

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.

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.

Ah, so you are referring to Haskell.

Amy pointers to documentation that's approachable by beginners?

https://www.youtube.com/watch?v=hhGnMbw98u8

https://www.youtube.com/watch?v=tfnldxWlOhM

https://www.youtube.com/watch?v=HnOix9TFy1A

https://pron.github.io/posts/tlaplus-curryon-talk

https://learntla.com/introduction/

https://leanprover.github.io/theorem_proving_in_lean/

https://rise4fun.com/dafny

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

https://www.betterworldbooks.com/product/detail/Building-Hig...

https://hillelwayne.com/post/pbt-contracts/

I recently started using Alloy for small models. Great for searching for constraints and state machines.