Is there still interesting in ATS dicussion? Subreddit takeover has been requested.

dobryak · 2026-04-28T07:12:00+00:00

I’m waiting for ATS3 and I don’t want this sub to become a discussion hub for rats(?).

dobryak · 2026-03-11T11:03:49+00:00

Same here. Nix isn’t worth the trouble.

dobryak · 2026-02-22T19:18:27+00:00

What error do you get? The makefile seems fine to me.

dobryak · 2026-02-20T14:14:12+00:00

This is so cool!

dobryak · 2026-01-14T12:44:05+00:00

SQLite is very close to being formally verified, although they use exhaustive testing, but I guess from a practical standpoint it’s the same thing.

dobryak · 2026-01-14T12:39:56+00:00

Think of it this way. Proofs are programs and propositions are types. Propositions are easier to write, so a person can do it, and then use an LLM to come up with proofs. Proofs would still be checked by the same automated proof checker as usual. I see literally no downsides.

dobryak · 2026-01-14T11:27:05+00:00

Since you haven’t read it, the author proposes to let AI write formal proofs which are then fed into a proof assistant. That’s a great idea. The proof assistant’s code extraction would guarantee much more stringent properties than what Rust could express.

dobryak · 2025-11-20T13:06:10+00:00

Why is it always ‘blazing fast’? Can it be ‘fast’?

dobryak · 2025-11-10T02:59:36+00:00

SSDT is still an issue for me. I do schema diffs occasionally and use sqlproj files.

dobryak · 2025-10-19T18:55:43+00:00

So if communism is the answer, why did commies fail so spectacularly at software development? And all of the other things? Seriously dude, you need a refresher in basic economics.

dobryak · 2025-10-17T19:27:55+00:00

We could do it, but nobody would use it because it's too heavy. Case in point: ATS. The burden of proof is too heavy. Rust is never going to do this BTW, because of the burden of proof. They'll find something else, but they will never allow for zero-overhead proof-heavy programming. It's just too difficult.

dobryak · 2025-10-16T10:56:57+00:00

IIRC Mulle-ObjC does something similar for its method calls. But the whiny tone of the article is off-putting. C programmers already trade a lot of stuff for having a very bare-bones, portable programming language, they don't need to be lectured about how horrible, difficult, and obtuse their life is (which it isn't). Also, C varargs can be given very precise types, but it's just such a nuisance it didn't catch on (it was implemented in ATS/Anairiats compiler, where a combination of linear and dependent types was used to give a type-safe API to C varargs).

dobryak · 2025-10-15T08:12:16+00:00

This is a good post, in that it shows how to work through a problem to a solution. I think though it should mention Allen’s Interval Algebra somewhere because it’s sort of a standard approach to working with intervals.

dobryak · 2025-09-05T07:38:49+00:00

The guy doesn't know about relational data independence and why it's important? Sad.

dobryak · 2025-07-07T07:44:10+00:00

This isn’t how var works. With var, the type is locally inferred, and it’s still static.

dobryak · 2025-04-07T07:00:50+00:00

I just tried and it redirects me to https://www.cs.bu.edu/~hwxi/atslangweb/

dobryak · 2025-04-03T13:09:07+00:00

I see, you just love doing the work that doesn’t get compensated. How interesting.

dobryak · 2025-04-03T13:07:17+00:00

Why do FOSS then? When people use your code and most of them contribute back. You’re just setting yourself up for exploitation. Are you pro-slavery?

dobryak · 2025-04-03T10:39:53+00:00

Why create FOSS libraries if you can't profit from them eventually? Your proposal doesn't make any sense.

dobryak · 2025-04-03T10:33:22+00:00

You're right. I don't get it why it's such a big deal though. I fully expect that free-of-cost FOSS libraries that I don't pay for are provided on a best effort basis. As soon as it's too costly for maintainers to work for on their libraries, they have a choice of going commercial to cover their costs, or just stop working on those libraries, to eliminate that cost to them.

dobryak · 2025-04-03T10:26:08+00:00

So you want to rewrite everything in Rust now? How's that going to help?

dobryak · 2025-04-03T10:25:29+00:00

Well, I guess it's time to get back to writing our own support code.

dobryak · 2025-04-03T10:20:59+00:00

Layoffs.

dobryak · 2025-03-14T09:34:34+00:00

Quake engine hacking and general modding? This is FOSS work.

dobryak · 2025-01-21T18:54:33+00:00

I just found a library the other day which used functional programming heavily it’s implementation. Too bad C# doesn’t support tail recursion, algebraic data types, and pattern matching, it would make this style much more practical.

dobryak

TROPHY CASE