Welcome, Guest
You have to register before you can post on our site.

Username
  

Password
  





Search Forums

(Advanced Search)

Forum Statistics
» Members: 4
» Latest member: trustedmedications2024
» Forum threads: 17
» Forum posts: 22

Full Statistics

Online Users
There are currently 9 online users.
» 0 Member(s) | 8 Guest(s)
Google

Latest Threads
BPython: an interactive P...
Forum: The Soft Side
Last Post by: Alexander
17 Sep 2023, 21:11:16
» Replies: 0
» Views: 121
GANDER – live mixes on se...
Forum: Music, Television and Film
Last Post by: Alexander
15 Aug 2023, 06:45:59
» Replies: 1
» Views: 315
Proof-of-concept for vali...
Forum: Sirius C*
Last Post by: Alexander
13 Aug 2023, 03:12:49
» Replies: 1
» Views: 269
About this forum
Forum: XAA Projects
Last Post by: Alexander
11 Aug 2023, 14:53:14
» Replies: 0
» Views: 150
Multi-distro support
Forum: Alabaster Linux
Last Post by: Alexander
30 Jul 2023, 23:10:42
» Replies: 0
» Views: 151
Project portal
Forum: Oración
Last Post by: Alexander
30 Jul 2023, 09:37:35
» Replies: 0
» Views: 168
Y2K is Forever
Forum: Village Pump
Last Post by: Alexander
24 Jul 2023, 01:58:56
» Replies: 0
» Views: 240
Quality Motion Music – Ex...
Forum: Music, Television and Film
Last Post by: Alexander
08 Jul 2023, 05:30:47
» Replies: 0
» Views: 223
Tohoku Minecraft Server
Forum: Digital Projects
Last Post by: Alexander
07 Jul 2023, 15:25:11
» Replies: 0
» Views: 177
Alabaster Linux
Forum: Digital Projects
Last Post by: Alexander
07 Jul 2023, 14:56:10
» Replies: 1
» Views: 323

 
  BPython: an interactive Python 3 TUI
Posted by: Alexander - 17 Sep 2023, 21:11:16 - Forum: The Soft Side - No Replies

I came across this project browsing the Papirus icon set. I find it very stimulating from a product design standpoint and thus felt compelled to share it here.

Home page preview:
[Image: scr.png]

Website URL: https://bpython-interpreter.org/ (archive)

Print this item

  Proof-of-concept for validating laws via transient variable lifetime
Posted by: Alexander - 11 Aug 2023, 15:20:31 - Forum: Sirius C* - Replies (1)

Let us have a program in C*:

Code:
typedef uint32_t myint;

/* Must be less than 100 and cannot ever equal 17 */
law : myint
{
   _ < 100;
   _ != 17;
};

/* Fibonacci sequence will satisfy both of those constraints, but how do we know? */
void fibonacci( void )
{
   uint32_t i, n;
   myint t0, t1;
   uint32_t tn;

   t0 = 0;
   t1 = 1;

   /* print the first two terms */
   fprintf(stdout, "Fibonacci series: %d, %d", t0, t1);

   /* print 3rd to 12th terms */
   for(i = 2; i < 12; ++i)
   {
      tn = t0 + t1;
      fprintf(stdout, ", %d", tn);
      t0 = t1;
      t1 = tn;
   }
}

Going through the Fibonacci sequence, we know that if we limit the number of terms to 12, we will never reach 100. But how does the C* compiler break this down?

It evaluates the possible values of each variable term that it is enforcing at every point they are modified, in an exhaustive recursive fashion. This means that the algorithmic complexity of verification is proportional to the algorithmic complexity of the program being verified. The verification algorithm will first minimise the possible program space by factoring in all constant values, which in the function above is very helpful.

In cases where the output of the function depends on outside variables, the laws applied to the incoming paramters are assumed to hold either directly or by marshalling, but beyond that, it will assume worst values for the type's size. In the case of complex algorithms, it will often happen that it is not trivial to guarantee the validity of a given combination of laws; for example, if a foreign n was given of type uint32_t, it may require brute force search to ensure that some other variable dependent on n never equals 17.

The default behaviour of the C* compiler in situations like these is to error out, asking the programmer to give it more certainty about the data it is dealing with. Practically speaking, this involves creating more concise types with more permissible laws. For instance, if you want to be sure a 40 bit integer never overflows via multiplication, you need to make sure the types multiplied to create it have a bit size that, summed together, does not exceed 40 bits. Like so:

Code:
typedef uint64_t outint;
typedef uint64_t term0;
typedef uint64_t term1;

law : outint
{
   _ <= 0xFFFFFFFFFF;
};

law : term0
{
   _ <= 0xFFFFFF;
};

law : term1
{
   _ <= 0xFFFF;
};

void mysubroutine( void )
{
   myout a;
   term0 b = /* ... */;
   term1 c = /* ... */;

   /* This is OK */
   a = b * c;
}

If the above code was modified to have laws that permit any valid addition or subtraction but not multiplication (ergo, the laws are only enough to allow linear mixing, not quadratic), then a = b + c would still be valid, but the compiler would error out if it found a = b * c. The precautionary principle is in play.

However, it will be possible to put the compiler into that brute force mode, potentially at great computational cost, in order to arrive definitively at an answer to that question. This is accomplished using a framework of satisfiability solver programs, which provide a bitcode proof that can be saved by a programmer for trivial verification of its satisfiability once the solution is found.

Print this item

  About this forum
Posted by: Alexander - 11 Aug 2023, 14:53:14 - Forum: XAA Projects - No Replies

XAA is an acronym that stands for Xion–Aquefir–Anodyne. It is a grouping together of project initiatives from Xion Megatrends, a hardware development company, Aquefir, a software development initiative, and Anodyne, a project to build a personal supercomputer from the projects in Xion and Aquefir.

There are many subforums in this forum. For the most part, they serve as bug trackers similar in form to the issues system from GitHub for the many software projects being developed for the XAA initiative. These softwares may or may not be open source. In general, we try to use the Artisan Software Licence which permits credited redistribution in a share-alike fashion, but not modification without the developers' permission.

Print this item

  Multi-distro support
Posted by: Alexander - 30 Jul 2023, 23:10:42 - Forum: Alabaster Linux - No Replies

Initially, Alabaster was only intended to target CentOS 7 and Debian 10, as both of these were the last stable Linux distros to support the Knights Corner Xeon Phi cards, of which I have so many and intend to leverage in building Grovercomp.

However, I also do other forms of sysadmin work, and have deployed Rocky Linux and Arch Linux on some new datacenter-leased servers that are in the throes of migration. Awkwardly, introducing Arch Linux breaks the previously clean dichotomy Alabaster had where some distros are non-GUI, while others are GUI-first, since it works just as well for both cases, and anyway, there’s nothing wrong with deploying Debian server-side anyway. To solve this, I am implementing two (2) variant scripts of the classic alabaster.sh one-liner: one CLI-only (headless) distro of Alabaster available at cli.alabaster.sh, and another GUI-first distro of Alabaster available at gui.alabaster.sh. As for the bare, unqualified original at alabaster.sh, it will offer an opportunistic script that will default to either GUI or CLI installation depending on your distro. For distros that can support both, it will ask you to wget from the new endpoints in order to choose.


For now, this is the support matrix:
  • Debian GNU/Linux [CLI and GUI]
    • Debian 10 (buster)
    • Debian 11 (bullseye)
    • Debian 12 (bookworm)
  • Open RHEL derivatives [CLI only]
    • CentOS 7
    • Rocky Linux 8
    • Rocky Linux 9
    • AlmaLinux 8
    • AlmaLinux 9
  • Arch Linux (rolling) [CLI and GUI]

Print this item

  Project portal
Posted by: Alexander - 30 Jul 2023, 09:37:35 - Forum: Oración - No Replies

Oración is a machine code assembler for both CISC and RISC instruction set architectures. Its initial development target involves supporting specifically the i286 and the ARMv4T instruction sets as a minimum feature level. Eventually, it can grow to support the current descendants of those ISAs, along with other architectures including RISC-V and novel ISAs created by Xion Megatrends.

A new assembler was deemed necessary at first to support arbitrary precision numeric modelling in the translation stages of Sirius C*. Later, it became clear that a new assembler was unavoidable due to Sirius DOS and A* proving to demand application of the concept of modular memory and khipus, as existing compiler infrastructure is far too bonded to the existing approaches of increasingly wide fixed-width integers for accommodating larger memory spaces.

Under the hood, it uses Backus–Naur–Nicholi normal form via an in-house C library to generate its own lexer and parser.

Additional resources:

Print this item

  Y2K is Forever
Posted by: Alexander - 24 Jul 2023, 01:58:56 - Forum: Village Pump - No Replies

I’m writing this thread today to shed some light on the administrative philosophy of this bulletin board, its attached wiki, and whatever sites beyond may crop up in the future. I have spent a considerable amount of time browsing the Worldwide Web by now, and I have attained a very nuanced perspective that is informed by niche “net native” communities like this one, “mainstream” sites called social media, and the real world (I am not a basement dweller, I am very married and esteemed IRL). Crucially, I also came of age in an era where Tumblr broke containment and kind of ruined everything, because so many people don’t understand that they are psychically attaching themselves to online communities and thus becoming vulnerable targets for dark triad psychopaths who want to exploit others and piss on digital rocks for a living. All of this has gone on far long enough, and I am tired of watching it happen over and over. The Worldwide Web might be a shitty, sometimes hostile place, but it was not this pathological, totalitarian state of gaslighting until about 2015 or so, depending on what corners you look in.

In the interest of completely destroying any chance that radical, cancerous culture has at forming any kind of metastasis here, I am instituting a rule that needs explanation: the year 2000 is forever. What does that mean?

If you’re old enough, you might remember it firsthand. And don’t worry, 2008 wasn’t that different either if we’re being real. I just went with this because it’s an old Geto Boys lyric, and marketing matters. But if you’re too young, this is something you probably know about in your gut but don’t realise what it is – all of the cultural pull towards the vapourwave aesthetics of the 1980s is no accident. You guys are yearning for those times when people simply posted, and I’m here to tell you that we are going back there, whether you like it or not. The truth is, if we don’t commit to say no to this psychic corrosion and stop mentally “logging on”, it is inevitable that this community, like so many others, will devour itself in the course of spontaneous drama about nothing to feed the malevolent impulses of a few terrible, broken people who should be seeking professional help instead of ruining online communities.

So, say it with me, and commit yourself to keeping the Worldwide Web usable and interesting forever: The year 2000 is forever. I want you all to log on here like it’s a random Tuesday afternoon in 2007, or 1997, or whenever, and stop taking the Web to be more than it is. We are not fully human beings on here – we’re just people posting messages with avatars behind keyboards and we could be anywhere from Stockholm to Bombay. And that has to be good enough, otherwise… there’s going to be nothing left on here worth logging on for.

Print this item

  GANDER – live mixes on set of Rüfüs du Sol
Posted by: Alexander - 13 Jul 2023, 08:29:29 - Forum: Music, Television and Film - Replies (1)

This guy tours various locations and does live DJ mixings of the discography of the popular EDM artist Rüfüs du Sol. They’re excellent mixes to listen to while programming, doing sysadmin work, or even cleaning house in my experience.

His channel can be found here.

Print this item

  Quality Motion Music – Extended Plays of the Weeknd
Posted by: Alexander - 08 Jul 2023, 05:30:47 - Forum: Music, Television and Film - No Replies

This guy found some stems I guess and made some absolutely ecstatic extended remixes of many popular singles by the Weeknd.

His rendition of Blinding Lights is intense. His YouTube channel can be browsed here. If you want high quality MP3s of his tracks, they’re behind a $1.44/month paywall on Boosty, apparently. Get ‘em while they’re hot!

Print this item

  Tohoku Minecraft Server
Posted by: Alexander - 07 Jul 2023, 15:25:11 - Forum: Digital Projects - No Replies

We host a dedicated Minecraft server!

Server IP: mc.tohoku.ac
Version: Java Edition 1.19.4 + Bedrock Edition via GeyserMC

Please be sure to follow the rules and have fun!

Print this item

  Alabaster Linux
Posted by: Alexander - 03 Jul 2023, 21:57:46 - Forum: Digital Projects - Replies (1)

This is the master thread for Alabaster Linux, a pseudo-distribution built on top of Debian and CentOS.

Print this item