Exotic programming language

[jankidudel]

Hello, I want to introduce you 1 of the most rarely used programming language: Mizar. I's developed in Poland, and is currently used only in 3 places: 1. Bialostocki University in Poland, 1 University in Japan and in Bialostocki university Branch in Vilnius(where i'm studying). So, some of the characteristics:

1. We haven't any books written about it(only poor little syntax documentation)

2. In some places spaces are possible to use(like around keyword or so), in other mandatory :D

3. It's something like maybe Prolog, but no, we must use THIS kind of *hit

If you want yourself look about it, please visit http://mizar.org/

[kbw]

Interesting.

I didn't see any code examples.

[hamsterman]

http://en.wikipedia.org/wiki/Mizar_system
Panašu kad šitas daiktas ne visai programavimui..
Butu įdomu pamatyti kodo pavyzdžių.

[jankidudel]

Here is 1 example


6 divides n|^3-n
proof
defpred P[Element of NAT] means 6 divides $1|^3-$1 ;
A1: P[0]
proof
0|^3=0*0*0 by power3;
then 0|^3-0 = 6*0;
hence thesis by INT_1:def 9;
end;
A2: for n st P[n] holds P[n+1]
proof
let n;
assume B1: P[n];
then 6 divides n|^3-n;
then consider i be Integer
such that
B2: 6*i= n|^3-n by INT_1:def 9;

2 divides n*(n+1) by Th3;
then consider j be Integer such that
B3:2*j= n*(n+1) by INT_1:def 9;

(n+1)|^3-(n+1)= (n+1)*(n+1)*(n+1)-(n+1) by power3
.= n*n*n -n + 3*n*n + 3*n by power3
.= n|^3 -n + 3*n*n + 3*n by power3
.=6*i+3*n+3*n*n by B2
.=6*i+6*j by B3
.=6*(i+j);
hence thesis by INT_1: def 9;
end;
for n holds P[n] from NAT_1:sch 1 (A1,A2);
hence thesis;
end;


// lt -> ne , cia labiau irodinejimams skirtas irankis, taciau yra kaip yra, vadinasi programavimo kalba

[Browni3141]

That looks confusing, but most languages are before you know anything about them. Does anyone know what language this is?
P=: p:([+i.@-~)/p:^:_1]1000 9999
dif=: 3 : '+./,2=/\"1 /:~"1|-/~/:~y.'
(#~ dif@>) (/:~@":"0 </. ]) P
+---------------------------------------+-------------------+
|1487 1847 4817 4871 7481 7841 8147 8741|2699 2969 6299 9629|
+---------------------------------------+-------------------+
The formatting is a little off.

[filipe]

I don't know, but if it isn't Perl it will make Larry Wall jealous.

[chrisname]

It's not Perl, I can tell you that right away.

[rapidcoder]

SED or AWK?

[Browni3141]

Sorry, not Perl, SED or AWK.
* is an interpreted language very good for mathmatical applications. Here's a shorter example:
+/\p:i.10
2 5 10 17 28 41 58 77 100 129

This is the cumulative sum of the first ten primes.
The last line is the result when the commands are run through the interpreter.

[hamsterman]

Could it perhaps be J ?

[Browni3141]

Yes, it's J. When I first saw it I thought it was some wierd error, but when you start learning it it's not so bad.