/tech/ - Technology★

https://pastebin.com/D8zdEmYH has some code written by the ATS guy himself.

My only explanation is that, before he developed ATS, he was employed for 20 years with pay based on LOC.

Contributed on ats-lang-users:

>A very crude hack for the "val () =" issue is to insert an extremely obscure symbol character in your code wherever you wish to write this and compile with a simple script that first replaces the character with "val ()=" before compiling normally. Also map the symbol to a rarely used key such as back-quote for convenience of typing.

I am foaming at the mouth.

>>846255 (OP)

There's no doubt that ATS looks unpleasant, and is probably unpleasant to write. It provides what is, AFAIK, a unique feature, however, which is the ability to formally specify and prove the properties of the code you're writing. So, unlike the seL4 kernel, which was written in C and then laboriously proven in Coq (over 200,000 lines of proof code for less than 10,000 lines of kernel code, IIRC), ATS is supposed to unite programming and proof. It's a neat concept, even if the language itself looks pretty rough.

But you'd use ATS in fairly restricted domains. High security kernels and operating systems, maybe networking stacks, that kind of thing. It's not what you'd use for manipulating text files or writing 2D games.

>>846291

Do they not understad M-w -> C-y?

>>846335

That costs you a lot of juggling when you use the kill ring for anything else. Try this:

http://www.gnu.org/software/emacs/manual/html_node/emacs/Abbrevs.html

Your code is less readable this way, though.

>>846337

Very cool. Thanks.

>>846318

Isn't Ada/SPARK exactly doing what you're saying?

>>846255 (OP)

Rust isn't ugly, it's cleaner than C or C++. It's not pretty though.

ATS on the other hand, now that's ugly.

I've looked at ATS, but the problem is there are exactly 2 people using it so it's impossible to get useful information about it and of course it has no libraries. It's really only useful to perform proofs on top of C programs. The proof system is neat but the syntax makes it unusable, and even the main author uses the gc instead of the pointer proofs.

>>846386

>cleaner than C

No.

>C++

Yes.

>>846376

No.

>>846397

C has less syntax elements, but the same fragment of code in C is a shitload dirtier since it tends to contain a lot of hacks and tricks to achieve even basic results.

>>846255 (OP)

>ATS's compiler names symbols after the the full path of the compile-time location of the files involved

what a piece of horse shit tbqh

#include "share/atspre_staload.hats"
#include "share/atspre_staload_libats_ML.hats"

datatype option0 (a:t@ype) =
  | option0_none (a) of ()
  | option0_some (a) of a

datatype list0 (a:t@ype) =
  | list0_nil (a) of ()
  | list0_cons (a) of (a, list0 a)

fun {a:t@ype} list0_last (xs:list0 a): option0 a =
  let fun loop (x:a) (xs:list0 a) =
        (case+ xs of
        | list0_nil() => option0_some(x)
        | list0_cons(x, xs) => loop x xs)
  in
    (case+ xs of
    | list0_nil() => option0_none()
    | list0_cons(x, xs) => loop x xs)
  end

implement main0 () =
  let var list = list0_cons("hello",
                 list0_cons("there",
                 list0_cons("friend",
                 list0_nil())))
      var last = list0_last(list)
  in
    case+ last of
    | option0_none() => print_string("no last to list!\n")
    | option0_some(last) =>
      (print_string(last);
      print_string("\n"))
  end

... the author's own code is still a mess though.

>>846318

>proof

That's just useless masturbation.

Either the output is what you want or it isn't.

>>847820

t. literal inbred

How does it compare speed-wise to say, Haskell?

type systems are for fucking nerds

go read a category theory textbook fag

>>857947

for speed, it beats the shit out of Haskell.

>>847820

ever write an assert() or any equivalent which is just "if this isn't as expected somehow, murder the user and hope we get away with it"?

proofs are the same thing but they throw errors at compile time instead of runtime, so you get to fix your code before deploying it.

ATS's default setting, on a scale of 0 ("do whatever the fuck you want") to 11 ("I have not run this code; I have only verified that it is correct.") is about a 4, because the normal indexing operators like somestring[3] require a proof to work at all.

>>866598

>ATS is faster than haskell

HAHAHAHA

All of the dependently typed languages are far slower than everything else except interpreted shit. Its not fundamental but its like saying Haskell is faster than C++ because the compiler has more guarantees. It may be true someday, its not now.

>>857964

I bet you are a big fan of javascript

>>866601

>All of the dependently typed languages

since ATS is hard, I've gone shopping a few times for a similar enough language. Idea: if I learn this, using its better docs or examples, I might then be able to come back to ATS and have an easier time, since it won't be so alien anymore.

language shopping result: nothing is similar enough to be worth the time.

ATS's proofs and dependent types have no runtime overhead at all.

>>866603

The proofs not having runtime overhead does not mean the language is faster for the same reason Haskell is not faster than C++.

>>866605

Indeed. That it beats the shit out of Haskell is just a fact, not something I've made any attempt to explain.

>for speed, it beats the shit out of Haskell.

If the goal is to be slow

>>866603

>nothing is similar enough to be worth the time.

Learn Idris. Idris is the most modern dependently typed language that is intended to actually be programmed in. It is also very nice for writing proofs.

>>866607

is Dons telling people to just lie outright if they don't know anything about a language? Such a nasty, mendacious little community that language has.

>>866608

I looked at Idris. It wasn't similar enough to be worth my time. ATS's programming with theorm-proving isn't there, and Idris (like rust) tries to prove things for you (termination in Idris's case) instead of giving you the tools to prove them.

>>866609

>termination in Idris's case

The termination checker is just for convenience you can turn of the checker. You can write your own termination proofs etc. The checker is just there because without proving termination of a proof your proofs can have errors in them. You must not know anything about the language.

>>866610

I know very little bit about--like I said, my interest was learning ATS, so when Idris didn't look useful for that I stopped looking into it.

>>866612

You should consider learning Idris instead then.

>>866613

The language that its supporters in this thread agree is slower than anything except interpreted shit?

Nah. I'll use the JS target if I want some ATS code to run slower than usual.

>>866616

ATS is dependently typed and fits in that "slow shit" category

>>866618

Since ATS is amazing for speed, this rule you have about dependently-typed languages is just wrong. Sounds like a self-serving myth, "Idris isn't bad; you just can't expect the same kind of speed from it."

>>866622

ATS is not amazing for speed. ATS is slower than almost every real language that is not interpreted.

>>866623

Yeah, you're just making shit up. This is THS. Since Idris is implemented in Haskell, I guess the same kind of dishonest creeps are interested in it. That's a pity.

>>866626

Only benchmarks that ATS does any good at are trivial tree operations that every functional language does well on

>>866628

Yeah, OK man. You're definitely going to lie your way into the big industry jobs. Since I've got a job, I'm going to stop helping you shit up this thread.

>>866631

>anyone that knows more about meme research languages than you is some unemployed loser

>>866628

http://web.archive.org/web/20121218042116/http://shootout.alioth.debian.org/u64/ats.php

that mandelbrot

>>866686

>that outdated benchmark

numbers from benchmark game 2014:

ATS: 24, C++ 19

>>866686

>That single core microbenchmark

>>866746

look, children. This is what rabid language partisanship reduces a human being to.

I'd like to learn it, but I'm really into FORTHs lately, and their simplicity and syntaxlessness makes me moist.

How big are the binaries? Is the language suitable for embedded code

>>866761

>one singlethreaded microbenchmark from 2012 is indicative that a language is fast

hahahahaha

>>866956

ATS won't let you index into an array without a proof and it has a lot of syntax, so it won't make you moist.

Small. Sure. ATS is probably slightly easier than Forth for embedded work since it can more easily exploit the popularity of C for embedded work.

I'm more interested in the other meaning of 'embedded' - injecting ATS into programs that already exist. It does this very well.

>>867034

>only pretending to be retarded

it's a page of benchmarks. The one I singled out is exceptional due to its memory usage probably because C++ is desperately trading memory for speed and still losing to ATS on speed. 2012 is not the 'before time'; I didn't pay a team of archaeologists to find these benchmarks for me. Turning your nose up at single(lol)core performance is like turning your nose up at non-VR games or non-quantum computing--it just means that you're a memelord without perspective and that your opinion is worthless--not an exercise in reason, but an exercise in recall ("which of these two things is newer and therefore better?").

>>867160

A few of those microbenchmarks are good because a single Chinese autist spent a shit ton of time writing the equivalent of assembly in ATS. If you do the equivalent in any language you will get the same results. Look at the code he wrote for those benchmarks that did well jesus fucking christ. Eventually autists in other languages did the same thing and well beat out the ATS performance.

>>867174

>a single Chinese autist

probably the author of the language, and it probably looks like complete shit because that's his normal style (c.f. the beginning of this thread) and not because he's actually doing anything that unusual.

>Eventually autists in other languages did [their perception of what he did]

yeah the benchmark 'game' is shit and it always will be shit so long as the people behind it are so sensitive to attacks on their honor. The important takeaway is that ATS beats the shit out of Haskell for speed :)

>>867182

>the person that wrote the compiler can write the equivalent of assembly in a microbenchmark and that proves the language is fast

hahahahaha

>>867184

>you thing ATS is fast because of [stupid reason]

No I think it's fast because I'm using it and can plainly detect that it's fast.

Meanwhile, writing 'the equivalent of assembly' in a dogshit language doesn't make it any faster. On the contrary, doing that in J or Python or JS will result in massive slowdowns.

What people actually do to make pigs fly is they go off and write a library in another, actually fast language, and then load that and do a benchmark that spends 99% of its lifetime in the other lang's code, and conclude that the pig is natively capable of flight.

This was really obvious when Haskell was doing it ("lol, you're using <the actual fucking string the language gives you and expects you to use>? Wow you're dumb. You should be using GHC.Only.Extension.String."), but there's also stuff like NumPy.

The approach the benchmark should've taken was to say that these extensions hybridize the language, and deserve a separate score.

... OK that's enough milking. Say something more than "hahahahaha".

>>867195

>The language supports the equivalent of inline assembly and therefore its fast.

Writing the equivalent of assembly in anything makes it fast

>>867199

epigrams of /tech/

#1. Dependently typed languages are much slower than non-dependently typed languages.

#2. Clearly-written code in a language is always slower than 'the equivalent of assembly' in a language.

go on. it's already funny.

>>867205

>>867205

>a languages speed is measured by microbenchmarks and not idiomatic code

>>867205

>Python is as fast as C because you can JIT assembly and run it