Melyik a kedvenc programozási nyelved?

Vala.

Egy C#-szerű szintaktikával rendelkező, kifejezetten Linuxos (GNOME-os) alkalmazások számára készített nyelv, ami a GLib osztályrendszerét emeli nyelvi szintre. A fordítója C-re fordít, amit a gcc fordít natív kódra.

Ha nem Valával foglalkoznék, akkor C-vel, Javaval, Javascripttel vagy Rusttal.

[link]

csatlakozom az elsőhöz

modern c++

Haskell -- régi szerelem ❤❤❤ -- , de az elmúlt két hónapban nagyon megtetszett az Agda ❤.

Az Agda és a Coq régi vágyam volt, de csak most jutottam el odáig, hogy apró léptekkel ugyan, de el is tudtam benne indulni.

Olyan erős típusrendszerük van, hogy akár matematikai tételek levezetésére is lehet őket használni --- és használták is már őket éles kutatásokban.

Én persze még itt nem tartok, én csak ujjgyakorlat jellegű dolgokat, pl. természetes számokkal kapcsolatos nagyon egyszerű algebrai tételek levezetését tudom kifejezni az ő típusrendszerükben: eddig a legbonyolultabb az összedás kommutativitása volt, és a jobbinverz létezése), de a lényeg az, hogy ezt **a típusrendszer** tudja kifejezni, tehát nem afféle futási idejű tesztről van szó, és hogy elvileg akármilyen erősségű logikai állítás képes fordítási időben, a program szerves részeként beépülni a kódba.

Itt nem csak az erő a lényeg --- végül is ezt egy jó unit teszt keretrendszer is nyújthatná, igaz, az futási, és nem fordítási időben --- de a lényeg még a fordítási időben való ellenőrzésen kívül inkább maga a szemlélet, amely a programfejlesztés menetét képes affelé inspirálni, hogy az ember meglássa a koncepciók mögötti algebrai összefüggéseket. Korábban is szórakoztam PHP-ban azzal, hogy algebrai adatszerkezeteket, sőt, a Haskell típusosztályaihoz hasonló dolgokat, monászokat szimuláltam afféle case classokkal és trait-ekkel: ezekből gyúrtam elő Maybe-t, Either-t, szóval efféle opció-és direktösszeg algebrai típusokat, de Agdában ennél is és a haskell-nél is szabadabb a horizont: megadatik elvileg minden, amit csak a Martin-Löf-féle típusrendszer nyújtani tud.

mátrixszorzás : ∀ (u v w : ℕ) → Mátrix ℝ u v → Mátrix ℝ v w → Mátrix ℝ u w

mátrixszorzás = ....

transzponált : ∀ (m n : ℕ) → Mátrix ℝ m n → Mátrix ℝ n m

transzponált = ....

transzponált-öninverz-tétel-biz : ∀ (m n : ℕ) (m : Mátrix ℝ m n) → transzponált (transzponált mátrix) ≡ mátrix

transzponált-öninverz-tétel-biz = ...