mmalone

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.

There's a problem with strings being lists in general because it forces a representation that's not perfect for every use case. Keeping strings abstract and giving them their own interface (even if it's very similar to list's) lets you optimize the representation, or even specialize the representation for different use cases. You can intern, use vectors, use ropes, use tries, or any number of other crazy things. It also lets you expand the string interface beyond the list interface.

Practically, certain operations end up being slow when you use the standard "strings are lists" mechanism provided by Haskell's standard library. Stuff like building a list is hard or slow for stupid reasons: Haskell uses cons lists with fast append-to-head and slow concatenation, so the common case of building a list by appending characters to the end is slow. Or you have to prepend and reverse. Stuff like that. It's dumb, but it matters.

The Haskell community has reacted by creating other ways to represent strings, like `Data.Text` and `ByteString`. These representations have certain benefits, so they're widely used. This adds _another_ problem: different libraries use different representations, so you end up having to convert back and forth between them all the time. Again, this is annoying and inefficient.

So yea. I think the lesson for language designers is clear. Strings are a distinct concept. Yes, they do list-like things, but they're not lists.

I've never worked on something "mission critical," but most common uses of recursion are tractable, so I'm not sure why it would be disallowed.

The simplest form of tractable recursion is where some argument in the recursive call is, by some metric, "smaller" than the outer call, and is heading towards a base case that terminates recursion when the argument reaches "zero." Two examples are: decrementing integers towards zero, and recursing on the tail of a list. You can prove termination and many other properties of such a function by induction. This concept is fairly easy to generalize to any algebraic data type, and to many other domains.

Edit: I realized I didn't really answer your question. The folks who are working on dependently typed languages (like Idris) see them as broadly useful, and they have a good point. Consider Java generics: they let you have types that depend on other types, like a "List of Integers." The compiler can make guarantees based on that type information and a lot of people consider that useful. With dependent types you can have types that depend on _values_, like "List of exactly 5 Integers that are all between 0 and 100." Again, the compiler can make guarantees based on that type information, and it could improve code safety, modularity, etc.

The challenge with dependently typed languages has been coming up with a "surface syntax" that's easy to use. Idris (and Agda) are pretty much state of the art there.

Yea... in theory it makes sense. In Haskell, field names are functions. If you have an instance of Human and you want it's name you do 'name human' not 'human.name()'. Polymorphism is done through type classes, not by ad-hoc overloading. So if you want the name function to take a Human or a Dog you need to define a type class with name and have both implement it (kind of like interfaces, but not really).

Pragmatically, it's really annoying. There's a solution in the space between pure (a la Haskell) and magical (a la Scala) that makes sense. I think Idris might have found it.

1. A geohash is a z-curve.

2. It won't be better than a k-d tree. Dimensionality reduction is usually done when you have really truly huge numbers of dimensions that are sparsely populated and you don't care much about some information loss (e.g., for machine learning) or, in this case, when you have an easy way to create a single dimensional index and you want to force multi-dimensional data into it. In the general case a k-d tree would be objectively better in terms of performance.

Yep. Geohash is just a fancy name for a z-curve.

True, but it is much better at preserving closeness than the alternative he mentioned (lexicographical sort).

If you're tempted to use space filling curves (z-curves, hilbert curves, etc.) you should take a look at simple multi-dimensional data structures as an alternative.

As a couple of people have mentioned in this thread, space filling curves aren't great at preserving locality (i.e., two points that are "close together" in two dimensional space might end up being "far apart" in one dimensional space, and vice versa). A k-d tree is easy to code up and, in general, will be more efficient for queries like k-NN than dimensionality reduction because it's better at preserving locality.

There are also good libraries for multi-dimensional data structures for pretty much any mainstream language.

See https://srfi.schemers.org/srfi-110/srfi-110.html. No idea why it hasn't shown up in a popular language (or maybe it has and I'm just naive).

I get what you're saying, but that's a pretty extreme view. Parenthesis are obviously syntax, even if they look similar to the notation used to represent ASTs in other languages. They are minimal syntax, but they're still syntax (also, lisps have `"@' and sometimes {}[]).

Just because this is the internet, I'll also disagree with your second point. Lisp programmers use white space and macros to make programs more readable. Despite this, lisp's adoption trails many less powerful languages that offer more intuitive syntax. Since lisp's metaprogramming facilities allow it to effectively simulate pretty much every other style of programming, the only explanation that I can come up with for this situation is that intuitive syntax matters a lot (at least for language adoption).

Why do you say it's for data? Doesn't racket use "reader macros" heavily for language syntax, or am I misunderstanding something?

Worse is better, amiright? sigh...

I believe Amazon uses commodity NICs + iptables in Dom0 (based on rumors). I have no idea what a custom ASIC would cost, but I think the Jupiter networking gear / Titan NIC that Google built are pretty advanced components that would cost more than commodity stuff.

In any case, the hardware components are fixed costs. What's not fixed is the cost of applying routing and segmentation rules for each packet. There are scarce resources involved here: the hardware has limited memory and limited cycles. You're paying for the use of those scarce resources (e.g., having a memory resident stateful firewall rule for a TCP session). Charging for bandwidth isn't perfect, but it probably correlates pretty closely with the underlying resources and is a much more intuitive unit-of-value for customers.

According to me... Are you arguing that it's not? It stands to reason that dynamic network architectures (SDNs) would be harder and more expensive to design and build than static architectures... it's the difference between managing shared mutable state and managing shared immutable state. On the hardware side, a simple commodity hub or switch is cheaper than a CPU, an FPGA, or burning your own ASIC to do fast SDN.

I'm not an expert, but it's possible... from what I understand amazon does SDN on CPUs in Dom0, Microsoft uses FPGAs, and Google has burnt their own ASICs... those are all expensive options. Much more expensive than generic networking gear. Possibly 4-5x, but idunno...

True, and it's still probably overpriced... but a lot of the SDN expense is in the stateful routing between networks (e.g., traffic going to/from the internet).

Keep in mind that with cloud providers you're also paying for the SDN that makes dynamic provisioning of VMs and logical network segmentation possible. Scalable SDN is much harder / more expensive than traditional networking.

For webapp <=> API it's pretty much the same as any other header, but with a subtle semantic indication that the value associated with the header is being used for authentication. Generally the value is a password or a bearer token. The problem is that this token is usually not channel bound (can be stripped and used elsewhere) and often has broad authorization associated with it. The security characteristics depend on lots of details. Usually when people say not to use HTTP Auth they mean don't send the username / password in base64 encoded cleartext over the open internet, as suggested by early HTTP RFCs.

The docs are sparse... but it looks like the answer is that it depends on what you mean by "correct." It doesn't look like it's a general purpose theorem prover, but it does appear to be model/spec-driven and the linked article says that the system can prove safety and liveness. I'm guessing they mean "type safety" but they may be using the term in the broader distributed system sense. In any case, it does look like it gives you certain "proofs for free" if your definition of correct is "eventually converges on a consistent state." I don't think you can prove arbitrary properties like you can with Coq or with a dependent type system. Still, very cool.

So... a business model around signed mobile code..? Neat, but I have many questions regarding safety: confinement, isolation, termination, resource management, etc. Shunting code around is the easy part... it's preventing code from doing bad/dangerous things that's hard. Need more info.

This seems right, except that Microsoft has clearly developed a higher level language than VHDL / Verilog for writing "virtualized network functions" that compiles down to something they can flash onto an FPGA (they call it Flow Tables in the presentation). So there's a higher level language that's, presumably, more intuitive for "normal" engineers to work with. When a new FPGA comes out the compiler is re-written and high level code stays the same. Basically the same thing we do with CPUs. So they're not _inherently_ hard to program.

SDN is common, and definitely a scenario where FPGAs outperform GPUs. Same for machine learning. (FWIW, Google uses ASICs for both of these use cases.) What we need is a high level language and access to FPGAs. I've been interested in business opportunities in this area, but it's hard to monetize. What's somewhat surprising is that the language bit hasn't been solved in the open source world either. My suspicion is that the reason an open source language like Flow Tables doesn't exist (AFAIK) is that there's not widespread access to FPGAs.

Do you think pure paradigms could be mapped, or are you skeptical of any general purpose language being able to efficiently compile to FPGAs _and_ CPUs (and GPUs)?

Why aren't more people deploying FPGAs like this? I started looking into using FPGAs for distributed systems work about six years ago when I was building a distributed database. Since then, about once a month I come across some problem that an FPGA could be useful for (i.e., enhance the performance enough that something otherwise infeasible becomes feasible). The devices themselves aren't that expensive (<$100) so why doesn't every server have one? Is there some hidden cost I'm not aware of (socket real estate, power consumption)? Or is it just a chicken-and-egg problem with not enough engineers asking for them because they don't know how they work because they're not more widely deployed?

I'm sort of bearish on most things blockchain but this seems like one of a very small number of things that zero-trust auto-executing contracts could be useful for. Someone could probably work out a mathematical proof of "if you transfer this much etherium the private key will be decoded." Heh.

In a sandbox environment (e.g., in a lab trying to deconstruct malware) they'll have a private DNS infrastructure setup to resolve all domains to some local IP address. That way they can intercept and reverse engineer the command & control traffic. The author of this malware tried to slow down security analysts by trying to resolve a "fake" (unregistered) domain. Probably just pounded on the keyboard and added a .com. The idea is that the domain should not resolve. If it does, it's an indication that they're in a sandbox / lab environment so the malware doesn't trigger. Again, this is an attempt to slow down analysis. Of course this was a stupid tactic because registering the domain and setting up DNS stopped the malware from triggering globally.

  > paranoid levels of security

  > # paste this into your terminal
  > # and get started in seconds..
  > curl -# https://usrfy.io/signup | sudo -sE

:O

I'm with you on this. I've never thought of JWTs as a session storage mechanism; rather, I've always thought of them as a simpler (JSON-based) alternative to technologies like X.509 attribute certificates and SAML assertions. If you're creating a ticket / verifiable claim, there are a bunch of security considerations that JWT at least lays the groundwork for, and that NaCl secretbox doesn't appear to offer. Curious what OP thinks about putting things like payload canonicalization, subject/issuer/audience specification, and expiration entirely in the user's hands. I suppose its up to implementors to do appropriate validation, but at least JWT simplifies the conversation a bit.

This. There are three (and arguably only three) common programming paradigms: imperative programming, functional programming, and logic programming with lineages back to Turing machines, lambda calculus, and formal logic / proof search, respectively. Languages can be broken down along other dimensions, but usually the term "paradigm" is reserved for the sort of irreducible foundation of a language, and these seem to be the three useful ones.

Edit: to put a slightly finer point on it, this irreducible foundation mostly has to do with how the language "computes." Imperative languages compute via statements that modify program state. Functional languages compute via proof reduction to normal form. Logic languages compute via proof search.

I'm curious... is it really true that an inconsistency would invalidate all proofs? Wouldn't this only affect non-constructive proofs (i.e., proofs that rely on the law of the excluded middle)? According to Wikipedia intuitionists also accept the principle of explosion... but it's not just an automatic result, is it? You'd need some proof or assumption that contradiction implies everything. Right?

> especially in the context of the space industry generally.

You mean the industry that landed a man on the moon inside of ten years?