Ranjit Jhala

Wow this was such an awesome viewing. I have found amazing work from the refinement typing folks at USCD. The book by Ranjit Dhalla is a gold mine! http://goto.ucsd.edu/~rjhala/lh-book-draft.pdf One question I had was can this be extended to type-drive "type" synthesis to derive new types and then use that to synthesize programs?

The very first blogpost http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refin… gives a very nice jargon and maths-free introduction to this. You don't need to know Haskell to follow it really. The assert function shown in the post is really cool. Amazing how easy it is to define a function that will compile time check an assertion (e.g. something is not "null"). That's code contracts done in the 101 class.

Thanks! It's great to see interest in our work on HN. Yes, this is the precursor to and basis for our current work on refinement type inference for C. For those who haven't seen it, our recent work has focused on extending the automatic program verification techniques shown in this talk to work for low-level programs - that is, programs that use mutable state, pointer arithmetic, and so on. The project page for our Liquid Types-based verifier for C programs is here: http://goto.ucsd.edu/csolve/ The project page for the overall Liquid Types project is here: http://goto.ucsd.edu/~rjhala/liquid/

This was a great talk! I was excited to see that there's (or was) some work being done to extend GHC to support this: http://goto.ucsd.edu/~rjhala/liquid/

If you want to see a dependently typed (technically, though the term often doesn't include this class of languages in practice) language which enforces smaller sets of properties more eloquently take a look at Liquid Haskell http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ The core idea here is called the Refinement Type which is basically what you're looking for. In order to power this type system Liquid Haskell depends on a full SMT solver, though, which is a rather large hammer to wield. As it regards to Peano arithmetic in DT languages the Peano naturals data type is awkward for doing math... but FANTASTIC for defining the properties of recursion and induction. Indeed, what you find is that the Peano nats show up everywhere as being a stable foundation for complex proofs and smart recursive functions. It's a very similar feature to Haskell's lists. Competent Haskell programers do not use lists when they want arrays or vectors—the latter types are naturally far more convenient when in their application space. But lists are not abolished! They're fantastically useful as control structures indicating sequential recursion. Typically you think of data types as forming their meaning through construction. You use numbers by constructing them according to arithmetic properties. Another way to do it, though, especially with recursive ADTs and inductive families, is to think of a type's meaning as being derived from how you break it down. The canonical way to break…

Btw, discovered something trying to update my research collection for memory safety and static analysis. Turns out, a prior technique for analyzing C that looked promising also has a Haskell project. That's Liquid Types. Links describing it & to various projects http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ C verifier download http://goto.ucsd.edu/csolve/

Liquid Haskell might be what you are looking for: http://goto.ucsd.edu/~rjhala/papers/real_world_liquid.pdf An example from that paper: type Nat = {v:Int | 0 <=v } type Pos = {v:Int | 0 < v } div :: Nat -> d:Pos -> {v:Nat | v <= n} The ATS programming language (http://www.ats-lang.org) is more ML-like than Haskell-like but can have ranged integer types. Something like: fun slice {n:int | n >= 1} (a:int n, b:list)

I've always hoped some language would have a prolog type system. Just today, I was pointed to liquid types [1,2] in haskell-cafe, and they look really promising in that respect. But the idea of having my compiler bail with a nice error message when I try: fibs = 0 : 1 : zipWith (+) fibs (tail fibs) fibPlus :: (int LESSTHAN 30) -> (int LESSTHAN 500000) fibPlus x = fibs !! x + 100 Is definitely too good to be true. [1]http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf [2]http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/

I didn't say Rust for Linux community, I said Rust community. Here's an example [1]. You don't have to search online forums and mailing lists very long to find countless others like this. The problem with the brigading (which has been done by the Rust for Linux community) is that it invites these zealots into the conversation. It's totally inappropriate and not at all constructive towards a compromise. Plus the stated goal of Rust for Linux is to enable people to write drivers in Rust, not to rewrite the whole kernel in Rust. Yet there are countless people in the wider Rust community that believe Rust is the future and every line of C code still in use should be rewritten in Rust. It's gotten so prominent that "Rewrite it in Rust" has become a meme at this point [2]. There are now many developers in other languages (C and C++ especially) who reject Rust simply because they don't like the community. [1] https://www.phoronix.com/forums/forum/software/general-linux-open-sour… [2] https://goto.ucsd.edu/~rjhala/hotos-ffi.pdf

> You may as well have said "then you use a magical tool that doesn't exist". Ok, so what this tells me is that you're not aware of what modern verification techniques look like. There's not really any one resource I can point you to, but take a look at these links. I've used these or similar technologies personally, but there are others I haven't used. https://en.m.wikipedia.org/wiki/Intuitionistic_type_theory https://en.m.wikipedia.org/wiki/Homotopy_type_theory https://leanprover.github.io/about/ http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf > What is your reason to think this is 'obviously' the case? Because I've done this, and anyone who claims to be familiar with formal methods should be at least passingly familiar with all the things I mentioned. Even if you aren't, if you've ever heard of SAT (a fairly universal CS concept) you should at least be familiar with the idea that non-exhaustive proofs are a thing.

For anyone who has the same reaction as I did when first hearing of this, "But isn't that just like a nullable value?" (don't worry, this post will not contain any monad analogies) Yes. Ish. In languages that have a null/nil/None then almost anything you have passed to any function could be null. Every function you write could have a null passed into it and you either have to do checks on everything or trust that other people will never pass those values in. That's pretty OK until something unexpectedly receives one and hands it off to another function that doesn't deal with it gracefully. In Haskell (and I assume others) this can only happen to Maybe types, they're the only ones that can have the value of Nothing. So the compiler knows which things can and cannot be Nothing, and therefore can throw an error on compilation if you are trying to pass a Maybe String (something that can be either a "Just String" that you can get a String from or a Nothing) into a function which only understands how to process a String. This feels like it might be restrictive, but there are generic functions you can use to take functions which only understand how to process a String and turn it into one that handles a Maybe. It's quite a nice system, even though I get flashbacks to java complaining I haven't dealt with all the exceptions. Haskell doesn't completely stop you from shooting yourself in the foot though, you can still ask for an item from an empty list and break things. There…

I'm sorry, I don't think I understand your message and my answer might be off as a result. Could you link to the current research on more general solutions than Checker, so I can get a clearer picture? > a type system limitation that every type describing side effects [...] can only be used in the context of a compiler/interpreter. A type system is just a logic description of a property that a program might have. It specifies how the language constructs interact with this property []. The fact that compilers use a type system is independent of your ability to write your custom type system, or to use it in a different context (IDE, toolchain, ..). [] Are you saying that a type system shouldn't be concerned by the AST of the language? An external type checker for Haskell: http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/01/01/refin… And the various type checkers for the not statically typed languages (python, ..) Also, I don't understand why you distinguish "typing side effects" as something different from the rest? > you need to write a different type system for each property But you do have to define your type system at some point? Are you thinking of something like Mezzo, where some userland properties can be defined without going down the type-system-definition road? https://protz.github.io/mezzo/ > But the interactions can, and should be more interesting, and take into account the order in which the callees are called etc. That's why…

In general, what you want to be able to mix types and values are dependent types (see languages such as Coq, Agda, Idris). However, dependent types are way too powerful, and as such extremely difficult to use. A light-weight form of dependent types are refined types, which are essentially dependent function types that have contracts on their parameters and return types. As refined types are way more limited than full dependent types (essentially, linear arithmetics, logic, and simple stuff like this), you don't always need to write the proofs manually but can use an automated theorem prover such as Z3. This is a hot research topic. There are attempts to do type inference for refined types - see [1] and [2]. The Liquid Haskell team is also exploring the issue of dependent types and laziness [3]. Below you mentioned that you want "soft casts" as well - check out [4], which attempts to do just that (implemented in language Sage [5]). I'm very interested in this topic as well, and have experimented a bit [6]; as it turns out, it's not that hard to implement a basic type-checker for simple refined types. It's also quite powerful - using Z3, even non-linear problems such as rectangular array access (mentioned by a poster below) are solvable, since you can trivially prove its safety using real arithmetics (which is decidable). The only big disadvantage that I see is the difficulty with dealing with state, but then again, even programmers can't reason about it properly; I mean,…

In the type-theoeretic world, you want to refer to "refinement types" [0]. Some interesting work that I have seen in this direction is Liquid Types [1][2]. There is some work in Haskell[3], but it is surprisingly very useful in Rust as well. [0] https://en.wikipedia.org/wiki/Refinement_type [1] https://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types… [2] https://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf [3] https://ucsd-progsys.github.io/liquidhaskell/ [4] https://github.com/flux-rs/flux

If you'd like to learn more about how the Liquid Types style of refinement types works under the covers, I invite you to read Pat Rondon's thesis: http://goto.ucsd.edu/~pmr/papers/rondon-liquid-types.pdf The UCSD Programming Systems lab has also applied refinement types to dynamic languages[1] and systems programming languages[2]. The MIT Computer Assisted Programming Group has similarly used liquid types-based techniques for program synthesis[3], while a group at Purdue has been working on maching learning of complex refinement types[4,5] that are difficult to state or infer using the liquid types techniques. [1] http://goto.ucsd.edu/~pvekris/docs/pldi16.pdf [2] http://goto.ucsd.edu/~rjhala/papers/low_level_liquid_types.pdf [3] http://people.csail.mit.edu/polikarn/publications/pldi16.pdf [4] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/ic… [5] https://www.cs.purdue.edu/homes/zhu103/pubs/pldipaper.pdf