kthielen

Ha ha, your short but diplomatic reply is a perfect example of the skill in question. Nicely done.

You make a very good point, and maybe a problem here is that “human factors studies” are set up like market research rather than anthropology.

People who’ve spent a long time programming have spent a long time optimizing everything about their work, and they’re willing to talk about it (most of them won’t shut up about it, even).

What do you have to say about Curry-Howard?

*moot

(No offense intended.)

Or ANS if you want an equally general packing to AC but you care about performance. ;P

For some reason you're willing to drop the context.

He's talking about people coming through the border without being vetted, who are dangerous to the country.

Do you think that people should be able to come into the country freely without any vetting at all?

He was pointing out a specific problem, maybe your imagination turned that into the much more general "all immigrants are bad" when he's never actually said or suggested anything of the kind?

If you say "they're eating the dogs, they're eating the cats, we have to clean up our country" then... yeah you're getting pulled into HR.

Trump was just repeating the same thing that many other people heard, a resident at a town council meeting in Springfield, Ohio claimed that some group of migrants there had eaten someone's pets.

Was it true? Who knows? People tend to repeat a lot of things they hear but haven't verified themselves. For example in that same debate, David Muir falsely repeated the lie that crime was down nationally. Do we take David Muir to HR?

That kind of obvious logical inconsistency, coupled with the assumption of moral authority (which for whatever reason seems to be the subtext for so many of these conversations), rubs a lot of people the wrong way.

And sure, it’s weird Hunter was involved but it’s also weird the guy who brags about being rich still won’t show us his tax returns […]

You’re so quick to drop the question of the Biden family’s involvement in Ukraine and you pivot to Trump’s tax return, but the billions of our tax dollars and lives lost in Ukraine now make that a MUCH more important issue than Trump’s tax returns.

Congressional investigations blah blah blah, obviously they can’t get anywhere. Trump was impeached for trying to get information right from the source, and it was very stupid. We should get that information, hopefully he takes another shot at it. We’ll see what happens.

[...] the Ukraine call [...]

Eh, maybe he shouldn't have been impeached for that call. President Biden's son had a strangely lucrative position, which he appeared not to be qualified for. And Biden was very involved in pressuring the Ukraine government to fire a prosecutor who was investigating that same energy company. There's a lot of public corruption in Ukraine, which was one of the factors leading to the election of their current president (according to what I've heard anyway).

This doesn't mean that Biden is definitely corrupt, but it does look very suspicious, and seems worthwhile to investigate. Our country is sending a lot of money to Ukraine. We deserve to know everything here.

Is it rare because it’s painful, or painful because it’s rare?

I made something like this for Morgan Stanley some years ago, a structurally typed eager variant of Haskell with static elimination of type class constraints (so no runtime penalty for overloading) and uses LLVM for the back-end: http://github.com/morgan-stanley/hobbes/

We used it for processing and analyzing billions of events per day. Using structural algebraic types let us encode market data (obviously) but also complex data structures inside trading systems that we could correlate with market data.

As you say, Haskell-ish expressions are much more compact and capable than SQL, which was one of the reasons I wanted to build it.

It also had a somewhat novel compression method (“types as probabilities” if you like the old Curry-Howard view), which was very important to manage billions of daily events.

Good times.

if you want to claim "forall x in X, P(x) is true" then you need to exhibit a particular element of x for which P holds

I don’t mean to be pedantic (although it’s in keeping with constructivism) but in the case you describe, you don’t have to provide a particular x but rather you have to provide a function mapping all x in X to P(x). It may very well be that X is uninhabited but this is still a valid constructive proof (anything follows from nothing, after all).

If instead of “for all” you’d said “there exists”, then yes constructivism requires that you deliver the goods you’ve promised.

I’ve always wondered why SQL doesn’t support variant types, and in this case especially.

If you’re going to store a sequence of values whose type can change over time, a variant is the obvious encoding choice. As new schemas are introduced, you add constructors to the variant.

On top of that, you can apply some basic structural reasoning to say eg a field can be indexed (possibly by different paths in each case) iff it exists in each constructor, or optionally with the awkward SQL nulls in case a field is not in each constructor (as they describe in the paper).

But then you could also use general variant deconstruction to decide on a case-by-case basis how to handle each version or subset of versions of a schema, and having that capability to represent variants in user data, independent of “evolving schemas” could have significant general use as well.

If you feel like having tuples and variants is too complicated, use dependent sigma types, so they’re all tuples, and then your schema language is much more expressive still.

It’s weird how much database systems have stagnated on this front.

I hear different opinions about whether type checking is "an" instance of abstract interpretation (AI) or "the" instance (which IMHO is a useful question since we might consolidate our efforts on one method if possible).

This article does a very good job of laying out typical examples motivating AI as a concept.

But the process of attributing points in the AI lattice to expressions does look a lot like type inference (and the AI lattice itself does look a lot like a type hierarchy).

Does this point to a slightly different approach we should take to type systems? For example, suppose the type of '1' was not 'int' but rather '1' (a type runtime equivalent to unit, but carrying its information at compile-time), and that 'add' is overloaded on input types so that it can either directly compute its result (also then statically knowable) or emit instructions to dynamically compute its result if its arguments are only dynamically known.

Is that the meta lesson here? Should we be using more detailed/nuanced type systems?

A career change, or a job change?

Ok but just make sure nobody else has to inherit it, and it’ll be fine.

Yeah, some maintenance projects have been much easier than others. Implicit knowledge that you have to “just” hunt down is generally the cause of difficulty and delay. It has little to do with “purity” and more to do with not wasting my time.

Just do some reasoning about the side effects.

"Wat?"

Have you ever inherited a 1MLoC codebase that you yourself didn't write from scratch, or worked on a large project with at least one other person? How do you know what the side-effects are and where they happen when you aren't intimately familiar with the code you're interacting with? That's the whole point of making effects explicit and available for analysis in the type system.

Lists and trees can be fully captured by sum and product types, but extending this representation style to DAGs and graphs doesn't work--you either get inefficiency (for DAGs) and then infinite regress (for cyclic graphs) attempting to continue the "syntactic" style of representation

You also need "inductive" recursive types to represent lists and trees, in addition to sums and products.

One way of representing the type of a list of T is like:

mu X.1+T*X

(Hence sum and product types, but also inductive or "least fixed point" recursion.)

But you can also use "coinductive" recursive types to represent "processes" (or "greatest fixed point" recursion) with almost the same notation:

nu X.1+T*X

This represents a FSM which at any point yields either a termination (the "1" on the left side of the recursive sum) or a value and a continuation (the "T" in "T*X" is the value and the "X" in "T*X" is the continuation).

This doesn't answer every question about graph representation, obviously, but it's a useful tool for attacking some graph problems you'd like to represent "syntactically" as you say (though you have to think in terms of "coinduction" instead of "induction" e.g. bisimilarity instead of equality).

I don't think they explained how it's different, I did listen to the podcast before posting my comment.

It's a pretty basic question that IMHO demands a clear and adequate explanation. If you read the 'abracadabra' example here: https://en.wikipedia.org/wiki/Assembly_theory

... you could be reading the abstract to an early paper explaining LZW codes.

Yeah but, how is an assembly index different than an LZW code?

Formal verification can work in areas where you have a long time to do development, or where your problem space is amenable to having a formal standard (like math problems). In most other cases it just runs completely opposite to the actual problems that software engineering is trying to solve.

Have you actually tried, or is this just the standard line?

I've heard this from people I've worked with, and when I followed up to ask what kinds of projects they've worked on with Agda, Idris, Coq, Lean, whatever, they had nothing.

I don't have anything either, other than that I've toyed around with some of these systems a little bit. But it seems to me like there's a lot of potential in dependently-typed programming, and we just don't have a lot of experience with it -- which is fine, but that's a very different situation than what seems to be the standard line, "all formal methods take a ton of time and are only viable in a few niche projects" (what are people imagining here? NASA space probes and stacks of binders? really it doesn't seem obvious to me, I'm not trolling).

Why would you post this here instead of the github page?

This piece focuses on complaints about ocaml, and the last half seems to just be syntax complaints (which I mostly ignore just because every language seems to have awkwardness in its syntax -- certainly Haskell, a language otherwise held up as an example, can be shown to accept some really weird text).

Good things about ocaml that I think should be mentioned are Hindley-Milner type inference (some might argue this, but it's a very effective system for inferring types), and also straightforward semantics (it's usually pretty easy to look at some code and make a reasonably accurate guess about what it will do on real hardware -- compare with Haskell).

I'm sympathetic toward the initial complaints here, which I also think are the most substantive. Type classes and qualified types, as in Haskell, would be very useful in ocaml/ML. The examples offered (show_of_int, show_of_double, ...) are valid, and also the related complaint that dishonestly broad types like structural equality (where runtime errors are raised for cases where the types are actually not supported) also make a compelling case for qualified types in ML.

I made this project ~10 years ago after making similar observations: https://github.com/morganstanley/hobbes

Things like structural equality and ordering are user functions here rather than magic internal definitions (e.g. equality is defined as a type class, and type class instances can deconstruct algebraic types at compile time to decide how to implement instances). But evaluation is eager by default, so it's pretty easy to reason about performance. And data structures can be persisted to files and/or shared transparently in memory with C/C++ programs without translation, also very convenient for the places where this was used. Actually we built some very big and complicated time series databases with it, used in both pre and post trade settings where ~15% of daily US equity trades happen. So I think these observations are useful and have passed through some pretty significant real tests.

Bulletproof counter argument, you sure showed me.

Programming is child's play compared to undergraduate mathematics taught in math departments.

One thing you might learn in math is to avoid making overgeneralized statements that you can’t support.

A valid substitution in your statement for “programming” is writing a compiler. And for “undergraduate mathematics taught in math departments”, basic differential calculus.

Yet we regularly teach smart high school students and first-year undergraduates calculus, and almost never try to teach them to write a compiler, contradicting your proposition.

But what do I know? I’m just a dumb programmer. I can’t read your mind, so maybe you had something a little more specific you wanted to say.

I think this is the goal of proof assistants based on the Curry-Howard isomorphism, which the original author thought to denigrate for some reason.

But I would advise taking time to consider whether it's actually, within the lens of yesterday (or 2 years ago)... good?

Other than to soothe egos, this almost never matters, because the person inheriting someone else’s code doesn’t live 2 years ago and can’t be blamed for not having the prior context (establishing that context is the job of the original author and is why documentation matters).

If you find yourself in the thankless position of having to reverse engineer intent and especially if you have an unsympathetic manager ready to lecture you about how you should magically read the mind of the original author, start looking for a new job and hack/slash away as much of the old code as possible to do the job that you’re asked to do.

Let me guess, that smug superiority, serious and knowing citations from "The Guardian", you're from the UK right? And you're lecturing us in the states about our naive skepticism of countries with royal families, while also paying your taxes to protect the royal pedophile Prince Andrew right? Please tell me more about how royalty no longer rules in Europe.

Yes, each thread produced several words.