Typed Assembly Language (2000)(cs.cornell.edu)

55 pointsby luu5 bulan yang lalu32 comments

cs.cornell.edu

Typed Assembly Language (2000)

https://www.cs.cornell.edu/talc/

36 comments

If you're gonna make a website for your programming language, you NEED to put an example of the language front and center on the landing page.

Three links deep and I finally found some code... packaged in a gz archive. I still have not seen a line of TAL

impl5 bulan yang lalu

This website is at least 25 years old. It uses one of the pre-canned templates from FrontPage 2000. Cut 'em a little slack. :-)

This was obviously someone's research project, and some of the papers have example code in them, e.g. see https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf.

hackingonempty5 bulan yang lalu

> This website is at least 25 years old.

That would explain why it only supports IA32.

geocar5 bulan yang lalu

> If you're gonna make a website for your programming language, you NEED to put an example of the language front and center on the landing page.

Did you consider the possibility that this sort of thing was done to avoid wasting time with non-experts who think an "example" of a language they don't know is enough to make comments about?

> I still have not seen a line of TAL

My suggestion: Start with the "Papers" and then look at the paper that introduces TAL. It has an example program with analysis

makerofthings5 bulan yang lalu

I’m an expert and I find it very frustrating when I don’t find some example code front and centre. It might not reveal the detail, but it sets the scene quickly and lets me know what sort of a thing I’m dealing with.

geocar5 bulan yang lalu

> I’m an expert and I find it very frustrating

So you say, but I think _I'm_ an expert too, and I wasn't frustrated in the slightest. Maybe you're just not an expert in this space. Did you consider that?

Of course it would be nice if everyone communicated to us in our preferred way, but I think making the reader work a little bit before they have a conversation is a good way to figure out if you're dealing with an expert or not, because an expert actually worth talking to about your ideas will not find it to be too much work to understand them

Students can especially benefit from this advice, because they are still too new to be able to recognise experts from the substance of their words

nananana95 bulan yang lalu

"I don't like having my time wasted" does not imply anything about one's skill in a field.

It's not 1995. Most of the internet is noise, and if you're showcasing something it's good form to immediately show your readers what actually is, and why they may or may not care about it.

Not showing the syntax of a programming language on the homepage of a programming language is poor communication. If you're OK with that - great, but not valuing your time and willingness to have it wasted in no way implies that you're an "expert".

[deleted]5 bulan yang lalu

geocar5 bulan yang lalu

> "I don't like having my time wasted" does not imply anything about one's skill in a field.

I have no idea what you think you just said, but I did not say anything like that.

> Most of the internet is noise, and if you're showcasing something it's good form to immediately show your readers what actually is

So you say, but without responding to either of my suggestions for not doing this, and after saying something that doesn't sound relevant at all.

Of what exactly are you trying to convince me to do? I'm not the author of this page, I'm not confused by what TAL is, and I'm not going to agree that you don't deserve to have your time wasted when you're here wasting mine, so what is it?

[deleted]5 bulan yang lalu

az09mugen5 bulan yang lalu

Same here, partial code from stackcodegen.ml in the said archive :

open Op;; open Var;; open Ctx;; open Ltal;; open Util;;

let debug msg = ();;

let rs = mkvar "rs";; let ra = mkvar "ra";; let rf = mkvar "rf";; let rt = mkvar "rt";; let rr = mkvar "rr";; let ru = mkvar "ru";;

let retty stackty aty = (Code(Ctx.from_list[(rs,stackty); (ra,aty); (rt,toptp); (rf,listtp); (rr,toptp)]))

let rec tt tctx ctx tp = match tp with Il.TVar a -> if bound tctx a then TVar a else lookup ctx a | Il.Int -> DTp Word | Il.Top -> DTp Top (* for now ) | Il.Tensor(t1,t2) -> Ref(Tcltal.mkpair (tt tctx ctx t1, tt tctx ctx t2)) | Il.Exists (alpha, tp) -> let beta = rename alpha in Exists (beta, W, tt tctx (extend ctx alpha (TVar beta)) tp) | Il.List t -> let tv = mkvar "list" in Mu(tv,NRef(Tcltal.mkpair(tt tctx ctx t, TVar tv))) | _ -> DTp(arrowtt tctx ctx tp)

and arrowtt tctx ctx t = match t with Il.Forall(alpha,t) -> let beta = Var.rename alpha in Forall(beta, W, arrowtt tctx (extend ctx alpha (TVar beta)) t) | Il.Arrow(t1,t2) -> let t1' = tt tctx ctx t1 in let t2' = tt tctx ctx t2 in let stk = mkvar "s" in Forall (stk,M, Code(Ctx.from_list[(rs,Stack(Tensor(t1',MTVar stk))); (ra,toptp); (rt,toptp); (rf,listtp); (rr,DTp(retty (Stack(MTVar stk)) t2'))]))

| _ -> tcfail "expected a function type in forall"
let typetrans tctx tp = tt tctx Ctx.emp tp let arrowtypetrans tctx t1 t2 = arrowtt tctx Ctx.emp (Il.Arrow (t1,t2))

( Need to specify the type ty of "the rest of the stack", in most cases alpha )

type code_env = {cctx : cctx; cs : code_section; fctx : Il.ctx; lctx : var Ctx.ctx; fp : int}

let get_fctx cenv = cenv.fctx let get_lctx cenv = cenv.lctx

type block_env = {cenv : code_env; ilist : instruction list; lab : clab; tctx : Ltal.tctx; rctx : Ltal.rctx}

let get_from_cenv f benv = f benv.cenv

exception CodeFail of string code_env exception BlockFail of string * block_env

(* val begin_fn : code_env -> clab -> register_file -> block_env val end_fn : block_env -> code_env val emit_label : fn_env -> clab -> dtp -> block_env val emit : block_env -> instruction -> block_env -> block_env val emit_end : end_instruction -> block_env -> fn_env val drop : reg -> block_env -> block_env val free : reg -> block_env -> block_env val push : reg -> reg -> block_env -> block_env val pop : reg -> reg -> block_env -> block_env val malloc : reg -> block_env -> block_env )

let do_print y x = (debug y; x)

let (>>) f g x = g(f(x)) let (>>=) f h x = let y = f x in h y x

let rec mkltp tctx rctx = Ctx.fold (fun t sk dtp -> let k = match sk with _,W -> W | _,M -> M in Forall(t,k,dtp)) tctx (Code (rctx))

let current_ltp benv = debug ("Generalizing "^(Ctx.pp_ctx (fun _ -> "") benv.tctx)^"\n"); ( rt is caller-save *) let rctx = update benv.rctx rt toptp in (mkltp benv.tctx rctx)

yjftsjthsd-h5 bulan yang lalu

HN Tip: Put 2 spaces in front of your text to get it formatted as code.

az09mugen5 bulan yang lalu

Thanks for the tip ! I'm very often on the phone for HN and I could not have done it easily. But I promise next time I'll post a big chunk of code I'll do it from my laptop, from where I can easily add 2 spaces at the beginning of each line.

az09mugen5 bulan yang lalu

Here is the code edited from my laptop ;)

  open Op;; open Var;; open Ctx;; open Ltal;; open Util;;

  let debug msg = ();;

  let rs = mkvar "rs";; let ra = mkvar "ra";; let rf = mkvar "rf";; let rt = mkvar "rt";; let rr = mkvar "rr";; let ru = mkvar "ru";;

  let retty stackty aty = (Code(Ctx.from_list[(rs,stackty); (ra,aty); (rt,toptp); (rf,listtp); (rr,toptp)]))

  let rec tt tctx ctx tp = match tp with Il.TVar a -> if bound tctx a then TVar a else lookup ctx a | Il.Int -> DTp Word | Il.Top -> DTp Top (* for now ) | Il.Tensor(t1,t2) -> Ref(Tcltal.mkpair (tt tctx ctx t1, tt tctx ctx t2)) | Il.Exists (alpha, tp) -> let beta = rename alpha in Exists (beta, W, tt tctx (extend ctx alpha (TVar beta)) tp) | Il.List t -> let tv = mkvar "list" in Mu(tv,NRef(Tcltal.mkpair(tt tctx ctx t, TVar tv))) | _ -> DTp(arrowtt tctx ctx tp)

  and arrowtt tctx ctx t = match t with Il.Forall(alpha,t) -> let beta = Var.rename alpha in Forall(beta, W, arrowtt tctx (extend ctx alpha (TVar beta)) t) | Il.Arrow(t1,t2) -> let t1' = tt tctx ctx t1 in let t2' = tt tctx ctx t2 in let stk = mkvar "s" in Forall (stk,M, Code(Ctx.from_list[(rs,Stack(Tensor(t1',MTVar stk))); (ra,toptp); (rt,toptp); (rf,listtp); (rr,DTp(retty (Stack(MTVar stk)) t2'))]))

    | _ -> tcfail "expected a function type in forall"

  let typetrans tctx tp = tt tctx Ctx.emp tp let arrowtypetrans tctx t1 t2 = arrowtt tctx Ctx.emp (Il.Arrow (t1,t2))

  ( Need to specify the type ty of "the rest of the stack", in most cases alpha )

  type code_env = {cctx : cctx; cs : code_section; fctx : Il.ctx; lctx : var Ctx.ctx; fp : int}

  let get_fctx cenv = cenv.fctx let get_lctx cenv = cenv.lctx

  type block_env = {cenv : code_env; ilist : instruction list; lab : clab; tctx : Ltal.tctx; rctx : Ltal.rctx}

  let get_from_cenv f benv = f benv.cenv

  exception CodeFail of string code_env exception BlockFail of string * block_env

  (* val begin_fn : code_env -> clab -> register_file -> block_env val end_fn : block_env -> code_env val emit_label : fn_env -> clab -> dtp -> block_env val emit : block_env -> instruction -> block_env -> block_env val emit_end : end_instruction -> block_env -> fn_env val drop : reg -> block_env -> block_env val free : reg -> block_env -> block_env val push : reg -> reg -> block_env -> block_env val pop : reg -> reg -> block_env -> block_env val malloc : reg -> block_env -> block_env )

  let do_print y x = (debug y; x)

  let (>>) f g x = g(f(x)) let (>>=) f h x = let y = f x in h y x

  let rec mkltp tctx rctx = Ctx.fold (fun t sk dtp -> let k = match sk with _,W -> W | _,M -> M in Forall(t,k,dtp)) tctx (Code (rctx))

  let current_ltp benv = debug ("Generalizing "^(Ctx.pp_ctx (fun _ -> "") benv.tctx)^"\n"); ( rt is caller-save *) let rctx = update benv.rctx rt toptp in (mkltp benv.tctx rctx)

addaon5 bulan yang lalu

I think a challenge to me for typing assembly, unless you’re doing old-school C style minimally-useful types, is that assembly types tend to be both more ad hoc and more transient than types in higher level languages, because these types come from the intersection of the problem domain and the way of expressing the solution, instead of just from the problem domain. In C++ I might have a type for “aircraft velocity in mm/s”, but in assembly I might have that type on one line, and then go to velocity in 2x mm/s the next line to save a renormalization; or have types for various state flags, but have them pack differently into a word in different places in the code. This is all expressible, but I think it would make me favor a more implicit typing with a heavier emphasis on deduction, just to minimize the description of types that exist but are not in themselves interesting.

noduerme5 bulan yang lalu

Just thinking about an aircraft's velocity as a specific type, rather than a vector with three floats, has my mind whirling. I can imagine a lot of terrifying things I wish I didn't think could be added later to that struct in some avionics system. What would you need a type for that for? Am I thinking too high level, where this type might include its own getters and function calls?

laszlokorte5 bulan yang lalu

Think of types more as physical units to check your calculation. The position on a chess board and on a checker board are both 2d integer vectors but you might or might not want them able to be summed together, the same way that 5 liters and 5 grams are both real numbers but should not be summed.

cubefox5 bulan yang lalu

So if your algorithm counts apples and counts pears, those wouldn't both have the type "integer". Far from it. They would have the types "number of apples" and "number of pears".

addaon5 bulan yang lalu

See the other replies — think physical units. An aircraft velocity is a three-vector, but not all three vectors are aircraft velocity. There are probably many different aircraft velocity types, but taking a typical one (NED alignment, mm/s scaling, some particular precision), the type is the set of three vectors that can, for example, be meaningfully added to each other. It makes sense to add two aircraft velocities; it does not make sense to add an aircraft velocity and a pixel color (another three vector), so they are observably different types.

noduerme4 bulan yang lalu

Any 3x3 vec (position 3, velocity 3, rotation 3) that would be more than that, a class specific to an aircraft, would be something much more. It would have position and velocity, and then it would have functions (getters, setters, or prediction functions). Something about the way OP said this was "a type" makes me very suspicious, because those raw values ought to be what you get when you poll the x vx rx ... of the type. If you're getting some sort of interpolation from that, it would obviously need to be from something which extended the type of an object in a certain position and attitude.

The reason I'm saying this is that this is exactly where terrible feedback loops occur, when a type may return an altered version of its basic data when trying to access the basic data.

If it's a type which has an underlying 3x3 vec and this type is specific to the aircraft so it has a bunch of overriding functions to operate on that data, that's fine, that's called a computer program. Not a specific type extending a vector.

ramses05 bulan yang lalu

    Temperature_C != Temperature_F != int8

It's apps hungarian v. systems hungarian all over again. https://en.wikipedia.org/wiki/Hungarian_notation#Systems_Hun...

[deleted]5 bulan yang lalu

chris_money2025 bulan yang lalu

Feel like this could be the solution to “LLMs will write in binary” Elon was talking about. The problem with it is, assembly is tightly coupled to the hardware, so LLMs might have an easier time generating/understanding context of a “typed” assembly language but now need to understand the hardware and its constraints as part of the context or have it in its training data. I personally just think having that knowledge codified deterministically in the compiler is simpler, but I guess time will tell.

throwaway274485 bulan yang lalu

What would be the advantage over generating human-readable code like, say, c? Why not just tell it what hardware you're targeting as part of the prompt?

chris_money2025 bulan yang lalu

In theory, you could create a hardware block that decodes text based assembly generated by an LLM, which would allow you to load the direct output the LLM produced into memory. In effect the LLM could write self modifying code on the fly without a compiler / runtime / operating system. Say if the LLM was a hardware chip itself instead of software, that’s incredibly powerful.

throwaway274485 bulan yang lalu

I suppose. But you could just as easily do this with C as the target language and then invoke a C compiler. Or just generate machine code directly. It's not clear what assembly specifically provides.

chris_money2025 bulan yang lalu

Assembly decreases the complexity of the hardware decode block significantly, lower complexity, better speed. C was created to reduce the cognitive load on the developer, with LLMs we don’t technically need to reduce cognitive load if we say compute isn’t a finite resource (it typically is but for sake of argument here).

Assembly is just more aligned to creating purely hardware primitives of LLMs and reasoning than C or upper languages

leptons5 bulan yang lalu

I feel like this is a solution in search of a problem that was already solved by C.

geocar5 bulan yang lalu

These "types" are hindley-milner types and have almost nothing to do with what C calls a type.

Your "feelings" may help you make snap judgements that can keep you alive, but they cannot help you code and they will conspire against you when you effort to learn new things. Nobody wants to feel wrong, and you will feel wrong many times when you learn something new, but it is the only way to actually learn the thing. Remember this the next time you have "feelings" about knowledge

throwaway274485 bulan yang lalu

So what problem is this solving? No need to be a dick.

geocar5 bulan yang lalu

> No need to be a dick.

But there was a need for you to characterise me so?

> So what problem is this solving?

What makes you ask me that instead of reading the website and papers for yourself? Do you think I could possibly know enough about the kinds of other problems you have from the example one that makes you call me names?

I mean, did you read even the first page of the paper I suggested? Were you confused by anything in the first paragraph? Do you know what System-F means in that context? Did you do an Internet search? Anything? Anything at all you could say you got stuck on that you didn't understand? Or did you somehow get the impression I should spoon-feed you?

Why do you waste anyones time with this?

leptons5 bulan yang lalu

You don't know me.

pjmlp5 bulan yang lalu

Except C being typed Assembly is a myth, first of all there were already high level systems languages during the decade that predates C, secondly there are plenty of CPU capabilities not exposed in C, if at all only via compiler specific language extensions, beyond the language standard.

Surac5 bulan yang lalu

Reinventing C?

fnky5 bulan yang lalu

You know it's good when all the members have their home addresses listed on their personal websites.

Too bad there's no examples of how this looked like.

[deleted]5 bulan yang lalu