Re: [ats-lang-users] Fwd: What is the goal of ATS?

[john s. <sk...@us...>]

On 09/04/2014, at 4:10 PM, Yves Dorfsman wrote:

> I am very new to ATS, but the verbosity is scaring me, although a lot of it 
> seems to be boiler plate that might be pushed away in templates?
> 
> I'm still trying to decide betwen ATS and OCaml...


If I may .. 

Ocaml is a great high level language with a good type system
and reasonable performance.  It is hardly compact, but it is
expressive, and easy enough to write software that actually
works (usually first time you get past the type system).

So Ocaml has a "prebuilt" compromise between correctness
and performance. It has a couple of major negatives though.
One is that building it requires a partial order of translation units
and recursion across units is very weakly supported so refactoring
is much harder than in C/C++. Another is that you cannot do
real concurrency: Ocaml threads interleave via a global lock.

ATS on the other hand is basically C with a better type system.
You can write very low level C like code without a lot of the scary
dependent typing stuff and then you will have code like C, that
will crash if you make mistakes.

If you use the high level typing stuff coding is a lot more work
and requires more thinking, but you get much stronger assurances
of program correctness, stronger than you can get in Ocaml
or even Haskell, and you can even hope for *better* performance
than C by elision of run time checks otherwise considered mandatory,
due to proof of correctness from the type system. Expect over
50% of your code to be such proofs in critical software and probably
90% of your brain power to go into constructing them rather than
just implementing the algorithm. It's a paradigm shift.

I would put it this way: most good programmers, when designing
and coding an algorithm have a mental reasoning or why they
believe their encoding is correct, and if there's a bug they usually
know in their mind its at the weak point of their belief stucture.

In ATS, you can concretise that mental reasoning and have the
compiler tell you when your picture is flawed, but doing so requires
a whole new workload, finding an encoding of those beliefs.

In this sense, Hongwei hopes the border between strong and weak
typing is fluid enough you can do fairly rapid prototyping and throw
in the strong typing after the fact where it  is needed. I think this 
claim remains open to examination and experiment.


--
john skaller
sk...@us...
http://felix-lang.org