These foundational versions of paradigms with small, useful amounts of primitives are also ideal targets for practicing formal verification. I’m saving this one for potential exercises in SPARK Ada or theorem provers if I learn them. With 60 operators, a verified APL looks quite doable. Also, it would be far from boring since the next move after single-threaded implementation would be verifying SIMD, multicore, or FPGA implementations to max performance. Might even be able to sell it if layering something useful on top given APL-style tools success in finance market.
We present the first formal semantics for [the array-computational] model, along with the first
static type system that captures the full power of the core language.
Our static semantics, a dependent type system of carefully restricted
power, is capable of describing array computations whose dimensions
cannot be determined statically. The type-checking problem is decidable
and the type system is accompanied by the usual soundness theorems.
Our type system’s principal contribution is that it serves to extract the
implicit control structure that provides so much of the language’s expressive
power, making this structure explicitly apparent at compile time
That’s really neat. Especially making it regular and work with SIMD/MIMD like I speculated about. You should make it a real submission next week in case anyone likes it who didn’t see this thread.
We really need an “apl” tag…
These foundational versions of paradigms with small, useful amounts of primitives are also ideal targets for practicing formal verification. I’m saving this one for potential exercises in SPARK Ada or theorem provers if I learn them. With 60 operators, a verified APL looks quite doable. Also, it would be far from boring since the next move after single-threaded implementation would be verifying SIMD, multicore, or FPGA implementations to max performance. Might even be able to sell it if layering something useful on top given APL-style tools success in finance market.
Here’s an interesting paper about typing array programs that I came across a while ago: http://www.ccs.neu.edu/home/shivers/papers/rank-polymorphism.pdf. Summary from the abstract:
That’s really neat. Especially making it regular and work with SIMD/MIMD like I speculated about. You should make it a real submission next week in case anyone likes it who didn’t see this thread.
I was about to do just that, but apparently it has already been posted here.