Yeah seriously. I'm surprised by the other comments here. It seems like people want loosy goosey typing that magically inserts lossy casts with convoluted semantics, as if they've been brainwashed by JavaScript and C.
577 karma · joined May 5, 2021
Type theory has many attractive properties over traditional foundations like set theory. See, for example: https://golem.ph.utexas.edu/category/2013/01/from_set_theory...
This Hacker News post is about a theorem prover based on dependent types. That's the context for our discussion.
> You will still have buggy programs in which you use those components
No one is disagreeing with this claim. But eliminating some bugs is better than nothing, even if you don't eliminate all bugs. You and the other commenters repeating this strawman are doing a lot of harm to people trying to socialize their research.
> Chances are you will be doing some new (=cutting-edge) math if you try to verify new things.
Citation needed. Most software is not doing anything interesting at all from a mathematical perspective, just shuffling data around. But either way the point is moot—Martin-Löf type theory (which is what this "magmide" thing seems to be based on) can do arbitrarily fancy math if needed (which is rarely).
I've been verifying bits of software for about 10 years, and I've never needed to invent new math to do it (though I would be happy if I ever did!).
Any large program will contain some smaller components with relatively well-defined behavior. CAD is not my specialty, so I can't really comment on what algorithms are used in that domain. Forgetting about fancy algorithms for a moment, just having a more expressive type system will allow you to express invariants in your code like the fact that array indices are within the relevant bounds, that you never try to pop an empty stack, etc.—everyday programming issues.
For a more concrete example, lately I've been using Coq to formally verify critical properties about a certain type of graph-like data structure I'm using in a system I'm building.
> If you are going for the easy parts, those can already be dealt with nicely with static typing and testing, essentially push-button automated verification.
Most engineers are already writing tests and using static types. Yet, we still have buggy programs.
And just to be clear, the kind of formal verification we're talking about is based on static typing. It's just a more expressive type system than what most programmers are used to.
> If you are going for the interesting parts, you will be doing math, essentially.
You are doing some form of math, but not the kind of cutting edge math that mathematicians do—which was my original point. You are not going to run into the kinds of tricky problems that mathematicians run into with theorem proving software, like universes being too small etc. Most data in software engineering is finite and reasoning about it involves little more than arithmetic and induction (which is just out of reach for mainstream type systems, but not for the kind of type systems used in proof assistants).
You don't need to verify the entire program for formal verification to be useful. You can adopt it incrementally.
The most common bogus argument I hear against formal verification is that it's impractical to come up with a spec or proof for the entire program, so we might as well not even bother with formal verification at all.
The kinds of theorems that we need to prove in software are much more elementary than what mathematicians are proving. I think software engineering can benefit from it long before mathematicians start doing cutting-edge math in it.
Rice's theorem states that those properties can't be automatically decided in general. But that's irrelevant to this discussion, because this "magmide" tool doesn't claim to do that. It merely checks proofs that have already been found (e.g., by a human), which is trivially decidable.
This tool does the former, leaving the latter up to humans.
No. Lean is good old fashioned Martin-Löf type theory. HoTT is that type theory + univalence + higher inductive types. Lean actually has proof irrelevance, which is incompatible with HoTT.
But the good news is you don't need HoTT to verify software. Type theory is already quite capable of it, despite what others in this thread would like you to believe.
> 5) Too much gratuitous abstraction. The old version was "everything is predicate calculus". The new version is "everything is a type" and "everything is functional".
Total functional programming with types is literally the same as writing proofs in intuitionistic logic, in a technical sense (the Curry Howard correspondence). This isn't a new fad. It's a deep result that was known more than half a century ago.
Decidability has nothing to do with this kind of formal verification. The tool doesn't have to decide the correctness of a program. The tool merely needs to check the validity of a proof of the program's correctness, which is rather trivial. Coming up with the proof is the hard part, and that responsibility still falls mostly on humans.
I think Go is the perfect example of this. On paper, it's a simple language. But:
- Not having sum types means it's awkward and unsafe to express concepts such as "X or Y". This is a big deal, because "Result or Error" is one of the most common ideas we have to deal with in programming. I think this tweet visually captures the awkwardness: https://twitter.com/GabriellaG439/status/1521860707444133888. Another place this shows up is pointers: in Go, since there is no way to represent "present or missing" at the type level, Go has to bake that possibility into the semantics of pointers. The billion dollar mistake.
- Every type in Go has a "zero" value. On the surface, this seems simple: when you declare a variable, you get a predictable value without having to explicitly initialize it. But this prevents you from implementing abstract data types which are guaranteed to be constructed by a smart constructor that establishes all the relevant invariants. Now you always have to worry about this zero value, since it might not satisfy the invariants of your data structure (consider the simplest data structure with an invariant: a pointer which is non-null!). Also, you can easily forget to set a field in a struct, which means the zero value will show up in unexpected places (resulting in subtle bugs that might go undetected even at runtime).
- Until recently, Go didn't have generics. Simpler, right? But that means if you want to build a reusable data type, you needed to either (a) make N copies of it, being careful to keep them in sync, with no help from the compiler, or (b) sacrifice type safety and represent data as interface{} (essentially a void* pointer), adding dangerous casts all over the place.
Languages like Haskell and Rust are more complicated than Go. But once you've paid the upfront cost of learning them, common programming patterns actually become simpler.
Of course, there's a flip side to this. Most languages have a lot of accidental complexity too, which isn't what my argument is about. So I almost hesitate to make this comment, fearing that it will be quoted out of context to justify adding badly designed features to programming languages.
(It is also true that structs are products. But that isn't relevant.)
Rust's popularity is certainly helping that, though I wish they hadn't repurposed the existing word "enum" to serve as a new synonym for a concept with an existing name ("algebraic data types").
1) I don't need you to prevent me from mutating this variable, just trust me to not mutate it.
2) I don't need you to ensure I handle every case of this enum, just trust me to update all the relevant code whenever I add a new case.
3) I don't need you to prevent me from reading the result without checking the error, just trust me to always handle errors.
4) I don't need you to track nullability in the type system, just trust me not to dereference null pointers.
5) I don't need you to let me hide the default constructor, just trust me to always use the smart constructor that establishes the invariants that I need.
6) Until recently: I don't need you to let me abstract away this type, just trust me to keep all the copies of the function/type in sync.
This philosophy may make sense for a low-level language like C, but not for a high-level language for building applications, services, etc. It amazes me that people voluntarily give up the guarantees of other languages in favor of Go for these use cases. It's almost as if the language wants bugs to slip into your code.
The problem is that sometimes the zero value is valid, but not special in any way and doesn't make sense as the default. Go has arbitrarily decided that one particular value is special without your blessing or the ability to override it. This leads to bugs in which the zero value shows up in places where you don't expect it, simply because there is some code which doesn't explicitly set it. That's a very easy mistake to make, which makes writing Go an error prone activity.
I shudder to think that there's probably some Go program that deals with money, and a user's balance might be cleared to zero simply because some operation forgot to explicitly set it in some struct.
In order to implement "optional" fields in Go where you want to distinguish between zero (a valid value) and none (a missing value), the common solution is to either put the integer behind a pointer (which can be null) or use some "sentinel" value like -1 to indicate that the value is missing (as long as that sentinel value isn't actually valid in the domain of discourse). These are terrible hacks, but exactly what you'd expect from programmers who spent the majority of their careers writing C.
This design also leads to another kind of issue: sometimes you don't want people to be able to construct values of a particular type without going through a constructor which ensures the relevant invariants hold. This concept ("smart constructors") is widely used in other programming languages, but it's impossible in Go because Go allows anyone to construct an inhabitant of any type simply by declaring a variable of that type.
A simple example of that kind of issue is pointers: in (safe) Rust, references are guaranteed to be non-null, and you use sum types to implement optionality. This is great because you can always dereference a reference and not worry about handling the null case. In Go, all pointer types have that nasty zero value (null), and there's nothing you can do about it. The billion dollar mistake.
I like the fact that Go encourages simplicity, and for the most part the language is fine. But I'm convinced that having every type be pointed rather than supporting proper sum types is actually more complex in terms of the implications it has on writing and reasoning about code. They have mistaken minimality for simplicity.
This seems like a mischaracterization of how addiction works.
Just to contextualize my explanation, I took it as a given that we were talking about the two _safe_ ways to handle missing data: a type system which has a notion of nullable/non-nullable types (e.g., Kotlin) vs. a type system which has Option<T> and no primitive notion of nullability (e.g., Rust).
I thought it was obvious that one would want this to be tracked in the type system _somehow_ (to prevent the billion dollar mistake), and that we were just discussing different approaches to achieving that goal.
1. Rust's traits are unary relations (i.e., predicates) on types, whereas Haskell's type classes support relations of arbitrary arity ("multi-parameter type classes").
2. Rust's traits do not support higher kinds, so you can't define many things which are considered pretty basic to Haskell programmers (Functor, Monad, etc.).
But despite these limitations, Rust's traits are still great and better than what 99% of other languages have.
The correct reasoning would be to recognize that certain language features make entire classes of bugs impossible. For example, in my Rust projects, I never have to worry about null pointer errors. Sure, there might be other types of bugs in my code. But at least I don't have bugs due to nulls. Also, there are no data races in my code—yet another thing I don't have to worry about thanks to the design of the language. (I'm not saying Rust is perfect. I'm just using it as an example.)
No, Optional is actually better than null because it's functorial. That means it obeys some common sense laws that one might intuitively expect. Instead of reciting the functor laws, I'll give you a concrete example.
Consider a `HashMap<K, V>` type with the following API:
get(key: K) -> Option<V>
However, if you try to do that with nulls instead of with Optional, it breaks if the value type is nullable, because nulls don't nest. For example, if your `get` method looks more like this:
get(key: K) -> V?
You might think to yourself, "that's silly, why would I ever want to store nulls in a map?" Well, here's one of many possible use cases: suppose you are using the map as a cache, and you want to cache the fact that something doesn't exist. This is called negative caching, and it's occasionally useful.
Or maybe you're building some generic code (like a collections library) that happens to use hash maps internally. If the hash map's get method uses a nullable type instead of Optional for its result, then it's likely that your library does not work correctly for nullable types, because it's easy to accidentally assume that null indicates that the key was not found in the map. That kind of bug won't be caught by the type checker.
Nulls are bad. Optional is good.
We really need to teach category theory to programmers so people can stop making this mistake which leads to error-prone APIs and code with hidden bugs.