Massive agreement. Wish: I wish that type-checking was built BESIDE languages instead of INSIDE-OF languages. Observation: While sitting through a reading of PLFA (Agda) [with CompSci Cabal], I developed the distinct feeling that I was looking at 2 languages, one for programming a type system, and, one for programming an implementation (an after-thought in Agda, IMO) ; to me, “Dependent Types” is just more-programming-language-constructs for a type language (DT adds parameters) ; Agda, et al, seems to be inching towards the re-discovery that type systems can be / should be programmed. The benefit of Relational Languages (PROLOG, miniKanren, etc). is that they specify “what is wanted” (relations) instead of “how to create steps for achieving what is wanted” (3GLs like Python, Rust, Haskell, etc.)

To me type systems are in the awkward position of trying to squeeze into an existing language (get out of the way), but also be powerful enough to express complex things like DSLs.

Type systems have to all sorts of optimizations to make unification manageable or querying the codebase.

Where it seems to me that these are solved problems - databases.

I imagine such a logic system that learns from the many decades of high performance databases, could be very fast (think indexes, query caching, materialized views etc.).

Rust embeds a datalog system in its type checker for borrow checking, if I’m not mistaken. github.com/rust-lang/datafrog

The only example of a language with a "sidecar" type checker is Shen (shenlanguage.org). It's a Lisp that includes a logic engine (roughly Prolog with lispy syntax), which is used to implement the type checker that can be turned on and off as preferred. And the type checker is just another Shen program, so nothing (except the effort) prevents you from substituting your own.

I'd also love to see static checkers outside of languages, allowing multiple checkers and in particular domain-specific ones. Ideally, I'd build my own checker as my understanding of my problem domain evolves.

I somewhat suspect that the traditional tight integration of type systems and languages comes from the benefit that type checking brings to optimization.

Yea adding project specific rules was the original inspiration that got me thinking beyond conventional type systems.

linters can work, but its duplicating all the work of the original type system, and usually don't even do proper type checking... and they usually have their own build step etc.

What if my additional rules could be understood by a common LSP-like system?

I somewhat suspect that the traditional tight integration of type systems and languages comes from the benefit that type checking brings to optimization.

There's no reason why the database generated from the logic language can't stick around to be queried for optimizations, right?

One thing that I imagine will require some work is interpreting errors (no answers found) for the results of running these programs. I'm imagining when this logic program runs it'll have to keep track of which queries / predicates succeeded & which didn't - and something to make something like a stacktrace, maybe even track that in a logic db that can also be queried to emit domain specific (nice) error messages.

I think the big idea is having a database that contains really detailed statically analyzed facts which can be used to check correctness, do optimizations, or even help with automated refactoring tools. So it might not even need to be 1 logic language, but a shared database system which all the logic languages can speak & store facts & query from.

There's no reason why the database generated from the logic language can't stick around to be queried for optimizations, right?

Technically, no. Socially, it means that the generation of important information is no longer under control of the compiler writer, and even language designer. They would have to cooperate with the users of their language and tool, and negotiate protocols for information exchange. It's more convenient to be a dictator.

It's curious that value types are so favored among all the useful summary/analysis operations we can do on programming languages. I mean similar techniques can track references, side-effects, entity life-cycles, resource usage, even evaluation of the language itself.

One reason types are built inside languages is undecidability. We tend to want the type checker to always terminate, and to err on the side of soundness rather than completeness. This is why the type language is weaker, whereas the "main" language can be Turing-complete.

I'd reverse the causality of that argument. It's because the type checker is part of the compiler that type checking has to be decidable and prioritize soundness over completeness (and lots of other nice properties we don't get, such as fitness for the application domain).

I don't know if I understand all the arguments against turing complete type systems. Could someone spell it out for me?

Is it hard that it'd be hard to debug infinite recursion in type systems? Do you worry people will misuse it to write fancy compile-time programs that will delay builds?

My second point seems to be possible in turing-incomplete languages too.

Something that I think would be unique to bringing in something like prolog is you could use its time travelling debugger to debug especially tricky types. I'd argue against tricky types/constraints in general, but when you're stuck with a library that goes wild with types you could at least dig in vs just getting a dump of useless text.

@Marcelle Rusu (they/them) The main issue with a Turing-complete type system is that the compiler might get stuck in an endless loop.

Turing-complete runtimes suffer from a similar problem. 😳

Turing completeness is indeed always a mixed blessing. But the problems matter more than the benefits at "meta" levels of scaffolding around a program. If you could get into an infinite loop before you even start running your program, the UX is much worse.

Hmm, going back to the original question it might work with some additional tooling. We typically have just a run command, but if the compiler supported running just the parser, or just up to the typechecker, maybe the UX becomes a non-issue. Yes, the programmer now needs to become aware of the internals of the compiler to some extent. But it might be a good trade-off.

I do think something like prolog might not be fit for it as the error messages seem poor, but it feels like a solvable problem - something like a stack trace instead of the "no" that prolog can give.

chalk looks pretty cool, thanks.

My fault, yet again. Where’s Jef Raskin when you need him?

Spaceships to explore pixels in products:

Scrubbing controls to cycle through:

• Different localizations side-by-side

• Data distributions that break layouts

• Theme variations that cause issues

• Screen sizes

These spaces are largely unexplored today only through manual means.

follow up question: does that distinction matter?

I think there's actually a trichotomy on that term that is worth exploring:

1) There's the industry standard, like "a11y", which I would say is basically always great to have correctly implemented on any production app; generally if the tool can be consistently navigated/manipulated keyboard-only and readable by assistive technology, it is a good sign the UI architecture is sound;

2) There's the interpretation you mentioned that would be designing with a particular user need in mind, like for instance, one can literally blindfold himself and optimize the tool for that particular usage context; that would quite surely make the tool "more accessible"; also, clearly great powers lie within optimizing for all human senses;

3) There's a third, quite literal, interpretation of "accessibility", as simply "having access at all to something". I personally have used that in the context of "live/visual programming can make technology more accessible", even simply because of ease of use, and mobile, etc. for instance.

I like that break down a lot!

Sort of 3 facets of one thing, but all different. I’m imagining a radar chart mapping them, now!

This seems like one of those many places where a noun obscures where an adjective would clarify. Tools are for folks, folks have abilities. How accessible a tool is for someone depends on fit. Not very satisfying, but at least phrasing it this way is in principle answerable in a concrete case. But "this tool has accessibility"? Or "this tool is for accessibility people"? Neither seems like a meaningful statement.

Kinda off to the side: I’d say that when making production stuff I take the kind of accessibility you’re talking about quite seriously, but when doing more research-y stuff I leave it aside during the initial phases because it’s so much harder to try new ideas while carrying the full weight of past standards.

but when doing more research-y stuff I leave it aside during the initial phases because it’s so much harder to try new ideas while carrying the full weight of past standards.

Do you think this is always true? (showing my cards my whole thing and job revolves around accessibility and sort of trying to advocate for it to be a core part of the design/considerations for stuff...not just cream cheese applied at the end, or blueberries shoved into an already baked muffin.)

As example of how it could contribute to the design of a thing:

• say you need some metric to track the impact of enhancing accessibility?
• an easy(ish) way to track this impact is to track completions wherein you define some set of tasks that can be completed within a system and then track what % of folks start the thing vs finish it
• leveraging accessibility-first design when approaching that situation empowers you to start thinking about "escape hatches," and ways to optimize for completion. Whereas if you just try to make it accessible at the end you'd remediate any keyboard traps you accidentally made, maybe with this approach you would ask "if someone were to get trapped at this step what would they do? what way out and through can we provide even if trapped?"

How I mean this is that if I want to experiment with, say, AR goggles, I’m not going to start from the position of “how will blind people use this display device?” Or if I want to build a two-handed input device, I’m not going to start from “how would a one-handed person use this?”

That said, there are many situations in more established input/output modalities (touchscreens, for example) where taking design cues from accessibility research improves the interface for everyone , which I think is broadly under-appreciated.

Word. That makes sense. Again, sort of showing my bias, I think across tech “accessibility” is often framed as a matter of input methodology when it could be framed as a core design principle, akin to color theory. I’ve found folks are more readily able to accept this idea when you don’t frame it as acceasiibility, but instead approach it like ~service design~ .

I am excited about seeing what apple does with AR/VR because I think desktop computing mostly ignore the human body (for both good and ill), phones and mobile devices started to force consideration of the body, and I ~think~ ar/vr could do some interesting stuff to ground computation into the body.

That said…all the talking and demos and reading I’ve done has me thinking that’s still a ways off

metadata-rich systems are well positioned for the kinds of introspection that make a11y easier…. e.g. this widget isn’t just a text box with a label, but a projection into UX space of a field object in a data dictionary somewhere. But metadata-richness usually leads to very poor legibility--every use case is an encoding in some lower-level language

I think we need a name for this more general design principle @Eli Mellen is trying to entail. I particularly like the tie to input (methods and contexts), because it makes it very tangible, and the emergent benefits can be often surprising (mostly thinking about programming interfaces here):

1) If my interface can be completely controllable/readable by voice, then any person (not only people with impaired vision for any reason) could use it in many arbitrary situations; I can program while cooking;

2) Similarly, if my system can be controlled completely by hand gestures, then I don't have to speak, or even touch the keyboard/mouse/touchpad; I can then build something very casually, like a game, using muscle memory alone;

3) Interesting research can be made on the ergonomics of interfaces considering arbitrary handicaps "Single Handed Programming", "Single Finger Coding", "Software Bending" (Programming using body gestures, which doesn't even exist yet), and their many design challenges' particularities;

4) The fact that one can program on the phone at all is a very sophisticated accessibility feat already, but (at least) that front gets talked about around as "Mobile First" design; still a very rare feat in current software ecosystem, especially for coding;

5) Repeat that for many devices (what about programming only with a joystick?) or body/mental state conditions (I have very little/high energy right now...) or environmental (would this tool be more helpful to code underwater?)... etc... etc...

These are a few examples of this unnamed phenomenon. I will try to compress it: "if you design with limitations in mind, the overall solution might improve".

What is the name?

I’ve run into this kind of thing and seen it called stuff like

• accessibility beyond compliance
• inclusive design (adjacent to participatory design )
• designing for resiliency
• …

But I don’t think they really capture what you are doing a great job of describing, @Samuel Timbó.

I wonder about something like reclaiming Interaction Design, but with a broader scope of what interaction encompasses?

It seems like more evidence that the software crisis never actually ended. We kind of just gave up on solving it.

en.m.wikipedia.org/wiki/Software_crisis

I take issue with the term "regular" for iOS and Google! They might be extremely widespread, but they don't seem to me in any way typical...

Things naturally cost more if they bring in more revenue. If you help to gradually bring in $100M/yr in revenue, $20M/yr will almost naturally stick to your palms. But that doesn't necessarily compare with efficiencies from an existential war 80 years ago (did the calculation account for inflation?!). In my experience revenues are justification for reduced efficiency. And none of this accounts for the value to society, which is a fraction of the cost if you could somehow (naive, I know) stop trying to think up new ways to juice revenues in user hostile ways.

Of course, how do you build just the valuable parts without the hostile parts? You got me..

(This comment partly inspired by the sprawling thread spawned by wandering.shop/@cstross/110989030686287315)

The whole idea that a project the size of Google search can be assigned a specific cost misunderstands how large software projects work.

Any sufficiently large software project eventually reaches a tipping point where it's too complex to refactor without breaking it. And at that point the complexity and cost of the system spiral out of control.

I work on a distributed database product that's built on SQL Server, which reached that point many years ago. Only a handful of people with decades of experience dare to touch the lower levels of the codebase - most of us just glue new pieces on top as best we can.

But if a project is lucrative enough, companies will keep shoveling in resources to keep it going. And the SQL org brings in billions, so Microsoft is fine with paying thousands of engineers to work there.

At that scale, it doesn't really make sense to talk about the cost of a software project, since it's bounded only by the revenue the product brings in.

And that applies even to a project like SQL Server, which is built purely to provide a service and (as far as I know) doesn't include "hostile" features designed to extract additional revenue from users.

@Personal Dynamic Media Now that I've read the link, I suppose this spiraling of complexity is what you're referring to as the "software crisis"? Do you think that's a problem that actually can be solved?

@Timothy Johnson I think spiraling complexity is a main part of it, but I don't claim to fully understand it.

I believe it can be solved by using smaller teams and technologies that increase individual productivity instead of technologies that try to protect hundreds of programmers from stepping on each other, like Java. I can't prove it, though.

I'm very fond of Seymour Cray's response to Thomas Watson Jr. From en.m.wikipedia.org/wiki/CDC_6600

The 6600 was three times faster than the previous record-holder, the IBM 7030 Stretch; this alarmed IBM. Then-CEO Thomas Watson Jr. wrote a memo to his employees on August 28, 1963: "Last week, Control Data ... announced the 6600 system. I understand that in the laboratory developing the system there are only 34 people including the janitor. Of these, 14 are engineers and 4 are programmers ... Contrasting this modest effort with our vast development activities, I fail to understand why we have lost our industry leadership position by letting someone else offer the world's most powerful computer." Cray's reply was sardonic: "It seems like Mr. Watson has answered his own question."

@Personal Dynamic Media Yes, there are large coordination costs when too many people are involved in a project. And that applies on the political side at least as much as the technical side - I haven't ever seen an effective decision get made if more than three people are actively involved.

But large companies are also wary of trusting any single individual with too much responsibility. They have to be prepared for anyone to jump to a different company at any moment. So just like the software, the organization itself is a distributed system with a high level of redundancy.

Startups usually can't afford to have that redundancy, at least in the early stages. I think they just accept a high risk of failure instead. And most of them do fall, but the handful that succeed are more productive by orders of magnitude.

@Timothy Johnson I think the secret there is to take Peter Naur seriously and make sure that at least three people in your organization always have the theory of the program. Once you get down to two or, God forbid, one, you put another person on the team and you make that person do the next five projects, with oversight and advice from the person who has the theory.