I'm sure there's a branch of programming where that would be amazing, but in my experience, I've never had major bugs due to my client and server implementing their protocol wrong.

In fact, I question most of the value of formal verifications for non critical software. Most of the problematic bugs that make it through in my experience are either a complex combination of multuple parts of the system interacting together in a way that doesn't end up behaving the way it was intended, or programmers implementing the wrong thing on edge cases.

Have you ever tried to change the protocol used by a running production system? I agree that in greenfield development an agile / iterative approach with a loose process works reasonably well. Once you have a running production system with lots of interconnected components, change gets really hard and really scary. Tools that help manage change in those cases seem useful to me.

Re: formal verification in general, most of the research has been moving towards making it easier to use and giving programmers some of the benefits of verification for free. I don't have any problem with the compiler telling me that my code is going to crash before the crash happens in production. That's unquestionably a valuable thing. Idris (and other languages) are trying to give you those sorts of benefits without reducing productivity or breaking your brain. It might not be there yet, but the progress is exciting.

Finally, both of the problems you identified (complex interactions and edge cases) are things that formal techniques are well suited to address... so I'm not sure how they support your case. Again, the only problem seems to be that the cost outweighs the benefits. But the cost is decreasing quickly.

I have 8 years of industry experience and feel the exact opposite. When programming in Ruby I am forced to not fully express the concepts in my head. We do TDD but our tests are humorously thin; typically covering none, one, many. Idris proofs are tricky but more automated and powerful than writing tests. And I can still write tests in Idris.

To go beyond "protocols", UI form data to server response back to UI display in a web app is a source of major bugs. So many things are broken. Recently I had to add a spurious lap infant to book a flight due to JavaScript template being broken when rendering 0 children.

What happens if you try to book 9007199254740993 spurious lap infants? Just curious.

I'd love to QuickCheck the diapers out of this method.

spurious lap infant?

True story: https://i.redd.it/lc84fv1lrv2z.png

You seem to just be thinking about low level network protocols.

The idea of a protocol in this sense encompasses pretty much any communication between things. This includes web service calls, user input via a UI, transactions between multiple systems, or even modules within the same program.

I've encountered so many bugs because of mismatches between server and client APIs, it's not even funny. Even then it remains a persistent problem, as evidence with changing Thrift schemas forward.

For write once and forget type of code like a website implemented by a contractor or throwaway code in Jupyter notebooks, the formal verification has a negative value indeed. For anything complex under maintenance ability to see that code behaves as expected in the edge cases without running it is invaluable.

> Think about being able to specify protocols in the type system and ensuring that your client and server meet the specifications. The example in that link is about user authentication. Imagine having a proof that the program can only get into a "LoggedIn" state by going through the authentication protocol.

Sounds like you are describing Session Types!

(http://groups.inf.ed.ac.uk/abcd/) (http://summerschool2016.behavioural-types.eu/programme/Dardh...)

Most functional languages have a type safe printf / sprintf (i.e. OCaml, F#, Haskell) which is similar to the effect you get in Idris: the types required to apply the function are statically analyzed from the format string.

Edit (links):

OCaml: https://caml.inria.fr/pub/docs/manual-ocaml/libref/Printf.ht...

F#: https://msdn.microsoft.com/en-us/visualfsharpdocs/conceptual...

Haskell: https://hackage.haskell.org/package/base-4.9.1.0/docs/Text-P...

The Haskell version of printf does not statically analyse the format string and will raise an exception if the provided arguments are invalid e.g.

    Prelude Text.Printf> printf "%d\n" "invalid"
    *** Exception: printf: bad formatting char 'd'

The behaviour of F#'s printfn is hard-coded in the compiler and could not be written in F# iteself.

Aren't the Ocaml and F# examples relying on some dedicated compiler support for the format string type, though? The Idris example is interesting because its printf implementation can actually be written in Idris.

The OCaml implementation used to be hard-coded in the type system, but has now been rewritten (in 4.02, I think) using GADTs.

https://ocaml.org/meetings/ocaml/2013/proposals/formats-as-g...

https://caml.inria.fr/mantis/view.php?id=6017

The compiler only does syntactic desugaring of format strings now.

> the types required to apply the function are statically analyzed from the format string.

Not so, in that Haskell package:

    Prelude Text.Printf> printf "%d\n" 1
    1
    Prelude Text.Printf> printf "%d\n"
    *** Exception: printf: argument list ended prematurely
    Prelude Text.Printf> printf "%d\n" 0.5
    *** Exception: printf: bad formatting char 'd'
    Prelude Text.Printf> printf "%d\n" 1 2
    1
    *** Exception: printf: formatting string ended prematurely

It could certainly be done with TH/QQ. I'm not sure, offhand, if there is already a package to that effect.

There are several packages on hackage offering a type safe printf. Some use TH, some use variadic functions (defined with a type class) or other advanced type level features.

Variadic functions are used in the package under discussion, and don't get you compile time checking of the format string.

Sure, and I know about those. I wasn't claiming that this was only possible in Idris -- and I don't think their implementations are nearly as clean or straightforward as the one in Idris.

In Idris, the pattern used to implement this is available to anyone that knows the language. It feels a lot more natural than using a macro system or typeclasses -- it is just functions.

One could also do this in D as well. it's not that impressive.

Does anyone remember the language that wanted to be future of programming, making everything (API calls, lists on screen etc) inherit from 1 base class, and it used SQL-like searching for filtering on collections?

It had a browser based demo.

Eve? http://witheve.com/

The Eve core is based on a distributed logic programming semantics (although SQL-like is a good accessible description). It was inspired by a datalog-based language called Dedalus (amongst other things).

Yes, thank you!

No but tell me if you remember.

Fortress?

Depressing thing to Google. Seems like an interesting project that couldn't keep it's funding in volatile times. It might have been Swift or F# if developed at a better company.

they did the best job of operator associativity and precedence i've ever seen. still hoping some other languages pick up on it. http://lambda-the-ultimate.org/node/2943#comment-43411

Whitespace-implied parenthesis.

    1+2 * 3 == 9

Sick! I wish Haskell notices this.

It's Eve

A haskell version of 1) is talked about here: https://www.reddit.com/r/haskell/comments/55bvt4/typesafe_pr... It uses the "singletons" library (no relation to the singleton design pattern) that emulates some features of dependent types.

If anyone is having trouble understanding the raw code linked above, the official book[1] introduces all three of those concepts gently and intuitively. I highly recommend it!

[1] https://www.manning.com/books/type-driven-development-with-i...

The book is written by the creator of the Idris language. I highly recommend it to those interested in type level programming as well.

Re typesafe printf, I assume the compiler can produce efficient code, since the pattern matching occurs at compile time?

Also, if you have an arbitrary string that isn't a constant that can be analyzed statically — for example, a string read from a config file — how do you prove to the compiler that it's a valid format-code string?

the compiler knows the failure modes. if the file doesn't exist, the printf isn't reachable. if the file isn't at least X bytes long, the printf isnt' reachable if bytes 10-20 can't be parsed as a number the printf isn't reachable.

it's just showing if you get through these 50 checks, by the time you get to printf the bytes will have been converted to what you need, or the program will have already errored out.

Any string is a valid format string.

I mean the combination of format string + values.

Anyway, is that really true? "%-1s" should probably give you an error, for example.

Type safe printf has been around for more than a decade, going all the way back to at least Groovy.

It is weird to me that so many people are getting caught up on the fact that type safe printf has been around forever. If someone has looked into Idris they almost certainly know that it isn't a new concept.

I linked it because its implementation is amazing comparatively and it is just one clean example of what is possible.

It's been almost a decade since I used Apache Groovy, but I don't remember its printf being type safe. Its method signature is

  void Object.printf(String, Object)

and it evaluates types at runtime.

I used it in OCaml well before there was a Groovy. But what's interesting here is that you get it without compiler special casing and without macros, as a natural consequence of how the type system works - in a way that generalizes to other problems.

>without macros

Type systems are macro systems, it's just not obvious because type languages are very different from expression languages. The main "innovation" of Idris is hammering harder on this front. And in any case, the fact that most type languages are logic languages gives people with a formalist bent a warm feeling in their stomachs.

There's a valid perspective from which type systems are particularly-constrained macro systems. That doesn't mean there aren't contexts where it's useful and/or interesting to distinguish. But if you wish, pretend I had written "traditionally conceived general purpose macros" :)

I know clang will not let you make a mistake, but it must be some kluge since the C language clearly doesn't anticipate that.

and then you need to log in a VIP user or a debug user without auth but cant produce a proof so now it wont compile at all. not a problem i you own the code but in client/server a third party could be the client or server so will have to be very careful about placing proof obligations on code you dont own.