<simpson>
isd: `COPY .` might not be what you want, FWIW, if you want reproducibility.
<simpson>
(Ultimately there's not really any substitute for serious reproducibility tooling like Nix.)
<isd>
simpson: yeah, COPY . . is maybe a bit imprecise. But the final tarball doesn't contain anything from the working directory anyway, and its means not having to specify every source file. If `git status` is clean, it should be the same thing.
<isd>
(.dockerignore is the same as .gitignore. I'm about to just make it a symlink).
<isd>
Re: nix, meh? at some point I'd like to just pin the exact image hash in the FROM directive. All Nix actually gives you is a determinisitc build environment; we're getting that by using a fixed docker container. We don't get the network isolation, but the go tooling doesn't do things that would make me want that.
<isd>
The go tooling isn't *too* far off from me being able to say "install this version of go and do go build with these flags" and have it work basically anywhere. There are a few things about the local system that end up in the binaries' metadata though.
<isd>
I'd much prefer to do the latter thing, as it seems more compelling to be able reproduce the build with relatively flexible environments; saying you have to build on system X makes system X a SPOF.
<isd>
But that proved to be a bit fiddly.
<isd>
It's a bit sad that a hammer as big as Nix is ever necessary for a project that with a fairly simple cookie-cutter build system.
<simpson>
I guess? I don't particularly understand why one would use Docker or Go.
<simpson>
But given that those are choices that have been made, Nix can still accomodate.
<simpson>
I suppose I'm mostly skeptical of non-correct-by-construction attempts at reproducible builds.
<isd>
re: Docker, in this case it's just useful to have a large library of base system images to start from. And the last time I tried doing sandstorm packaging with nix, the base system was big enough to be prohibitive; sandstorm apps package the whole filesystem. With docker you have e.g. an off-the-shelf alpine image that's easy to extend, which is small enough that you can get reasonable package sizes without trickery like what spk dev
<isd>
does (which is *really* terrible for reproducability)
<isd>
Go has good support for capnproto, and various archive formats/basically everything else needed in the standard library. It's also really easy to build static executables, and to cross compile -- that dockerfile builds MacOS binaries, which for many other languages would be an ordeal to figure out how to do on a linux system at all, much less reliably. Windows should be fairly easy to support to; the build doesn't get any more complic
<isd>
ated, and writing the code is one of the things where "it might already work, I just haven't tested it."
<isd>
I really get why lots of people don't like the language itself. but the tooling and libraries around it are amazing for a lot of use cases.
<simpson>
Sure.
<simpson>
It's always surprising to me that folks don't find dealbreakers with languages. I'd think that folks would want to be able to quickly discount a language.
<isd>
That seems really cynical to me; I don't find myself looking for excuses to not like something. There are dealbreakers, sure. But it seems odd to come into something with an attitude of "I'm going to find some reason not to do this."
<isd>
I actually *do* like the language. But I acknowledge there are some deep, valid criticisms of it.
<simpson>
Well, yes, I *am* really cynical. Also I don't have the self-hatred required to write piles of code in mediocre languages.
<simpson>
And going looking is one thing, but the bad languages will make things obvious. Lua, for example, is blatant about being 1-indexed; Go is explicit about having both no generics/templating, *and* also seventeen numeric types.
<isd>
The 1-indexing thing is stupid, but hardly seems like it should be an absolute dealbreaker unless it really causes a problem for a given problem domain. I've toyed with a lot of languages and I've never seen one that's perfect -- that's a pretty mild flaw as things go.
<simpson>
It's a problem because Lua *also* silently returns `nil` on invalid table lookup, so any code which accidentally does 0-indexing is silently broken.
<simpson>
And sure, most languages are bad. Special case of Sturgeon's Law.
<isd>
Yeah, silent nil is a *really utterly horrible* thing. That's I think a more defensible dealbreaker.
<isd>
Re numeric types in go, really? it's just the standard machine types + bignum libraries. That's pretty standard, except in languages that prevent you from accessing native machine types -- you really need that in a language designed for doing low-level programming/writing high-performance code.
<isd>
Re: generics, it does seriously hamper the language's applicability, and I don't use it for domains where it really causes a problem. But it's always a question of trade-offs.
<isd>
fwiw, they're actually talking about adding them for go 2.
<simpson>
Sure. But, y'know, compare and contrast: Monte has *two* numeric types, Int and Double. Go has `complex128`, which could be a library type. Also `uintptr`, because pointers were such a good idea~
<isd>
And just Int and Double is a reasonable spot in the design space. But it is actually really inappropriate for the kind of software Go is intended for.
<simpson>
Ooh, I'm interested in this. What other types might be interesting?
<isd>
Fixed size integers of common lengths are really important when you're writing network code/anything that parses binary formats. You can do it in other languages, but it's clumsy. Also, if you're trying to write high-performance code, having access to low-level machine operations is important, so any language in that space really should expose the numeric types the machine can deal with directly.
<isd>
Honestly, I'd like to see a language that just throws floats out the window and uses rationals everywhere -- they're utterly horrible to reason about. But it wouldn't be a systems language.
<simpson>
Monte, like Go, isn't a high-performance language, but a high-level far-from-the-metal language.
<simpson>
I've been working on a proper rational/computable-real story for Monte. It's possible to have fast rationals, using quote notation.
<isd>
Go is very much intended and used for performance-critical applications.
<simpson>
That's what I heard when I learned it at Google, but AFAICT it's really more of a playground for the team that builds it.
<simpson>
I dunno. Monte puts security before performance, and it's *really* weird to think of inverting that again for any cloud-oriented languages.
<isd>
I would agree for Monte the pile of numeric types that Go has doesn't makes sense. But thre's no such thing as a "general purpose" language.
<simpson>
Oh, sure. Monte's meant to be Blub; shitty as hell but somehow better than its peers nonetheless.
<TimMc>
I like how many numeric types Rust has. :-)
<simpson>
But we just haven't found that to be a problem in practice; our in-practice problems are things like "transforming a tree takes a long time" and "compilers are hard".
<isd>
Again, different problem domains.
<isd>
Rust makes pretty much the same decisions re: numeric types.
<isd>
But that's a pretty standard set for any language that's going to let you work with machine primitives.
<simpson>
Sure. And, again, I don't understand choosing performance over security. (Monte doesn't have `unsafe` blocks either.)
<simpson>
On the flip side, do Go or Rust have tools for doing prefetching, for doing explicit SIMD, etc.?
<isd>
IIRC Monte doesn't have a static type system?
<isd>
I think rust has SIMD intrinsicts.
<simpson>
Correct. Monte's very much like E.
<isd>
Honestly, I think no type system is a bigger problem from a security standpoint than anything I've seen wrt numeric types...
<simpson>
How so?
<isd>
My experience is that good type systems catch a huge percentage of the bugs I've had creep out in to the wild in untyped languages. Dwarfs numeric-related bugs by far.
<isd>
I can't really follow the code snippet you linked btw; want to clarify what it's doing?
<simpson>
It's a test function. The first assertion is checking that the types line up and that strings aren't Words (because they aren't Ints); the other assertions are about 8-bit arithmetic.
<isd>
...all things that any type system would rule out a-priori
<simpson>
Our experience is that Monte, like E, has a confinement property (in this case, inherited from lambda calculus) which is far more powerful than most type systems.
<simpson>
Huh? Type systems can't demonstrate that arithmetic works. Types are lower bounds on correctness; tests are upper bounds on correctness.
<isd>
Confinement is orthogonal to type system though; I agree it's powerful, but you can have both.
<simpson>
Sure. And there are typed members of the E family. But Monte is not one of them.
<isd>
(Haskell is the one example I can point to).
<simpson>
On the flip side, we have an *auditing system*; it's possible to write programs called "auditors" which inspect the ASTs of other objects.
<simpson>
So we can mechanically prove that an object is transitively immutable, or that it can be traversed as if it were a primitive container.
<isd>
Prop tests are also good, especially for algebraic properties. No argument there. But you literally said "The first assertion is checking that the types line up and that strings aren't Words".
<isd>
Looking closer at the test, yes, the other things aren't something a typical type system would cover.
<simpson>
Well, sure, when testing a guard (an object which performs a type assertion), guards really only can do a couple things (pass or fail) so it's worth checking that failure works correctly.
<simpson>
That's the fun of being untyped; we can have whatever type system we want, as long as we build it.
<isd>
When I say "type system," I mean static types -- if it doesn't happen at compile time it's not what I'm talking about.
<simpson>
Ah. Monte compilers *can* do whatever they like, but they're not obligated to optimize or prove anything.
<isd>
I'm definitely not the sort of person who thinks types are a panacea; they're one tool in the toolkit. But they're a powerful one, and while there's a big design space, I don't think "no types at all" is a good spot in it.
<simpson>
Sure, understandable. Monte only does this because it's how computer networks work; the filesystem and network are fundamentally type-erasing.
<simpson>
So by being unityped, we get to have a *uniform calling convention*; everything is an object, and objects communicate by sending messages, even across the network.
<isd>
My experience with optional type systems is that they tend to feel bolted on, and end up being much less powerful.
<simpson>
Definitely less powerful, but also more powerful? You'd need dependent types to match snippets like m`def f(g) :List[g] { return [] }`
<isd>
Explain what that snippet does for me?
<simpson>
It's a function which takes a guard and returns an empty list.
<isd>
what is a guard exactly?
<simpson>
It claims that its return type is m`List[g]`, a list of whatever-g-is.
<xet7>
My experience with Go is that is crashes very easily. That was a nice way to fail a work project some years ago. Shooting foot with machine gun.
<simpson>
A guard is an object with one method, .coerce(val, ej). A guard either allows the value through, possibly unwrapping it, or calls the ejector to indicate failure.
<isd>
xet7: yeah, that is one thing that I really do have a problem with in Go
<isd>
People talk about generics, but the presence of nil is orders of magnitute more important, and so avoidable...
<simpson>
xet7: Error handling in Go is pretty frustrating. I wish that Go had a feature from E, *ejectors*, objects that perform a non-local exit when called.
<simpson>
In E or Monte, one can write m`f(ej); g(ej)` instead of `_, err = f(); if err != nil ...`
<simpson>
isd: In object-based languages, it might be unavoidable. Certainly in Monte it's not possible to forbid utterances like m`object null as DeepFrozen {}`, and there's not really a good way to have a lack of return value.
<isd>
Agree with the error handling thing, it is painful. But it's also a lot easier to get right than any exception system I've seen. I haven't encountered a satisfying design in that space.
<isd>
The way to avoid null is to have proper sum types.
<isd>
You certainly can't avoid "this is the wrong sort of thing" at runtime if you don't have static types. but it's really not hard if you do.
<simpson>
We have those now! But we used Zephyr ASDL, which supports nullable values.
<simpson>
But yeah, the guard fun doesn't stop there. m`List[Int > 2]` is legal; list of integers, where every integer is greater than 2. m`Not[List]`, anything which isn't a list.
<isd>
If you're checking it at runtime though, it's just a fancy assertion. Better than silently accepting bad data for sure.
<isd>
But you can certainly still do that sort of thing in a typed language if you can't manage to capture the invariant statically.
<simpson>
Sure. Typed languages could, in theory, catch up to untyped languages in terms of expressing contracts.
<isd>
myFun list | any (<2) list = error "contract violated" ; myFun list = ...
<isd>
I mean, for that matter you could just change the above to myFun list | all (>= 2) list = ... and let the pattern matching fail otherwise.
<isd>
Or if you were doing this kind of thing all the time write a helper funciton `require condition = if condition then True else error "Contract violated!"` and then just `add | require <condition>` to a function. And then your'e basically there.
<simpson>
Basically, yeah. All that's needed is the compiler support.
<isd>
Which is not even that hard to come by.
<simpson>
Maybe? As a compiler author, I don't think it's trivial or easy.
<isd>
And I mean, even in python I could just make the first line of my function assert all([x >= 2 for x in list]) at the top of my function. It's just a few extra characters, and adding the compiler support is a trivial desugaring.
<simpson>
Sure. Python *could* have used their annotation syntax to support a powerful and expressive contract system.
<isd>
..and you could even do much of this as a library with decorators and helper functions; wouldn't be too hard to make a library that lets you write @contract(...). Like, this isn't even something you need language support for.
<isd>
and it doesn't get harder by adding types.
<isd>
There's just less stuff to check.
<simpson>
Sure. And if we didn't use guards for auditions, then that might be a path for Monte. But tightly integrating guards into our syntax allows for some guard information to be available during audition.
<simpson>
Which enables, say, the `DeepFrozen` auditor to prove transitive immutability, by showing that every captured name has a guard which enforces immutability.
<isd>
immutability is another thing that is totally coverable by a type system; Rust does this.
<isd>
(Haskell too, but somewhat trivially)
<isd>
But you can more generally do that kind of thing if you have reflection support, which is orthogonal to type systems.
<simpson>
Sure. Auditors are written in Monte, though, so they can be arbitrarily powerful. I have about half of an auditor for primitive recursive arithmetic, for example.
<isd>
Though it is more common to have it in an untyped language because you need to have the information available at runtime for safety checks anyway.
<simpson>
No reflection here, just audition. Objects have rights; they have private closures, they can refuse to consent to certain kinds of inspections, etc.
<isd>
Wouldn't be hard to design that into the reflection system.
<isd>
Like, that sounds like a useful mechanism, but again it's orthogonal to types.
<simpson>
Maybe it's possible using e.g. Bracha's mirrors.
<simpson>
Sure. At the end of the day, Monte's still untyped. It's a major design goal.
<isd>
Maybe we can run our own IRC logger when botbot.me shuts down.
<xet7>
I did reorder Wekan Platforms wiki page to make Sandstorm first and ask for supporting Sandstorm because I would really like to keep Sandstorm Oasis running. https://github.com/wekan/wekan/wiki/Platforms
<isd>
xet7: thanks for the link to that talk by the way; just got done flipping through the slides, and it was interesting.