The actual current site, pre-nuke
root
parent
581371b073
commit
e2e8d2ed42
Binary file not shown.
Binary file not shown.
Binary file not shown.
64
article.php
64
article.php
|
|
@ -4,18 +4,49 @@ $slug = $_GET["slug"];
|
|||
$servername = "localhost";
|
||||
$username = "local";
|
||||
$password = "";
|
||||
$dbname = "articles";
|
||||
$conn = new mysqli($servername, $username, $password);
|
||||
|
||||
$article_query = "SELECT * FROM articles WHERE slug = ?";
|
||||
//$keyword_query = "SELECT * FROM keywords WHERE id = ?";
|
||||
if (!function_exists('mysqli_init') && !extension_loaded('mysqli')) {
|
||||
echo 'We don\'t have mysqli!!!';
|
||||
} else {
|
||||
echo 'Phew we have it!';
|
||||
}
|
||||
|
||||
$article_query = "SELECT title, author, description, keywords, updated FROM articles WHERE slug = '?'";
|
||||
$keyword_query = "SELECT keyword FROM keywords WHERE id = ?";
|
||||
|
||||
if ($conn->connect_error) {
|
||||
die("Database connection failed: " . $conn->connect_error);
|
||||
}
|
||||
|
||||
if (!($stmt = $conn->prepare($article_query))) {
|
||||
echo "Prepare failed: (" . $mysqli->errno . ") " . $mysqli->error;
|
||||
}
|
||||
|
||||
$stmt->bind_param("s", $slug);
|
||||
$stmt->execute();
|
||||
$article = $stmt->get_result()->fetch_assoc();
|
||||
|
||||
$stmt = $conn->prepare($keyword_query);
|
||||
$stmt->bind_param("i", $article['keywords']);
|
||||
$stmt->execute();
|
||||
$keywords = $stmt->get_result()->fetch_assoc();
|
||||
|
||||
$conn->close();
|
||||
|
||||
$article_content_file_location = "/var/www/html/articles/" + $slug;
|
||||
$article_content_file = fopen($article_content_file_location, "r") or die ("404 File not found!");
|
||||
$article_content = fread($article_content_file, filesize($article_content_file_location));
|
||||
fclose($article_content_file);
|
||||
?>
|
||||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charset="utf-8" />
|
||||
<meta author="<?php echo $article['author'] ?>" />
|
||||
<meta name="description" content="<?php echo $article['description'] ?>" />
|
||||
<meta name="keywords" content="<?php echo implode(',', $keywords ?>" />
|
||||
<meta name="description" content="<?php $article['description'] ?>" />
|
||||
<meta name="keywords" content="<?php implode(',', $keywords) ?>" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
<title><?php echo $article['title'] ?> - Lijero</title>
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
|
@ -40,11 +71,26 @@ _paq.push(['enableLinkTracking']);
|
|||
<body>
|
||||
<nav>
|
||||
<div id="navbrand">Lijero</div>
|
||||
<ul>
|
||||
<?php foreach ($navbar as $navitem) { ?>
|
||||
<li><a href="<?php echo $navitem['url'] ?>"><?php echo $navitem['name'] ?></a></li>
|
||||
</ul>
|
||||
<ul><?php foreach ($navbar as $navitem) { ?>
|
||||
<li><a href="<?php $navitem['url'] ?>"><?php $navitem['name'] ?></a></li>
|
||||
<?php } ?></ul>
|
||||
</nav>
|
||||
<article>
|
||||
<header>
|
||||
<h1>
|
||||
<h1><?php $article['title'] ?></h1>
|
||||
</header>
|
||||
<?php $article_content ?>
|
||||
</article>
|
||||
<footer>
|
||||
<div class="metadata">
|
||||
<span><img alt="Author" src="//lijero.co/res/icon/person.svg" /> <?php $article['author'] ?></span>
|
||||
<span><img alt="Updated" src="//lijero.co/res/icon/clock.svg" /> <?php $article['updated'] ?></span>
|
||||
<div class="license">
|
||||
<a rel="license" href="http://creativecommons.org/licenses/by-sa/4.0/">
|
||||
<img alt="This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License" style="border-width:0" src="/res/cc-by-sa-small.png" />
|
||||
</a>
|
||||
</div>
|
||||
</div>
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,187 +0,0 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charset="utf-8" />
|
||||
|
||||
<meta name="author" content="Lijero" />
|
||||
<!-- <meta name="description" content="" /> -->
|
||||
<meta name="keywords" content="Lijero,code,operating system,distributed,network,resource graph,abstraction" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>Beyond Operating Systems - Lijero</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
_paq.push(["setDocumentTitle", document.domain + "/" + document.title]);
|
||||
_paq.push(["setCookieDomain", "*.lijero.co"]);
|
||||
_paq.push(["setDomains", ["*.lijero.co"]]);
|
||||
_paq.push(['trackPageView']);
|
||||
_paq.push(['enableLinkTracking']);
|
||||
(function() {
|
||||
var u="//p.lijero.co/";
|
||||
_paq.push(['setTrackerUrl', u+'foo']);
|
||||
_paq.push(['setSiteId', '1']);
|
||||
var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];
|
||||
g.type='text/javascript'; g.async=true; g.defer=true; g.src=u+'foo.js'; s.parentNode.insertBefore(g,s);
|
||||
})();
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<div id="navbrand">Lijero</div>
|
||||
<ul>
|
||||
<li><a href="/">Home</a></li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
<header>
|
||||
<h1>Beyond Operating Systems - Abstracting Over Networks</h1>
|
||||
<div class="metadata">
|
||||
<span><img src="/res/icon/person.svg" alt="Author" /> <span class="author"><a href="https://lijero.co/about/lijero">Lijero</a></span></span>
|
||||
<span><img src="/res/icon/clock.svg" alt="Date" /> Posted 2017-10-06</span>
|
||||
</div>
|
||||
</header>
|
||||
<h2>Introduction</h2>
|
||||
<p>
|
||||
I've come to get my crazy idea smashed apart. Or open an innovative discussion! Whatever it is, I don't wanna waste your time so I'll be brief. Let me know if anything needs clarification, since I'm shrinking a couple notebooks into one article.
|
||||
</p>
|
||||
<h3>Programs running on the internet itself</h3>
|
||||
<p>
|
||||
I want to write software for the whole internet! That can mean a lot of things, though:
|
||||
<ul>
|
||||
<li>Websites without a host</li>
|
||||
<li>Multiplayer games and apps without even <em>thinking</em> about servers</li>
|
||||
<li>Easy distributed stuff like cryptocurrencies</li>
|
||||
</ul>
|
||||
</p>
|
||||
<p>
|
||||
Operating systems mean we can write software for <em>any</em> computer but I want to write software for <em>every</em> computer at once! A <strong>globally distributed operating system</strong>.
|
||||
</p>
|
||||
<h3>Building up to a global OS</h3>
|
||||
<p>
|
||||
It's gonna take a lot of layers of abstraction. Bear with me, I'll get there eventually!
|
||||
</p>
|
||||
<h2>Step 1: The Resource Graph</h2>
|
||||
<p>
|
||||
If you're going to write a distributed operating system, it better <strong>not matter where data comes from</strong>. So <strong>unify every resource</strong>, from memory to files to HTTP calls, into a <em>resource graph</em>. That said, you can't make assumptions about your surroundings either: <strong>implicit dependencies have got to go</strong>.
|
||||
</p>
|
||||
<h3>Unifying resources</h3>
|
||||
<p>
|
||||
We still need to know what data is, which can be pretty tough when you don't know where it's coming from. The solution is an <strong>extremely strong type system</strong>. The type system tells software what data actually is. That said, different resources have different properties, so this has to be expressed in the type system as well.
|
||||
</p>
|
||||
<h3>Killing implicit dependencies</h3>
|
||||
<p>
|
||||
This is where the resource graph comes in. A graph is just a general way to structure data. It's basically a generalized filesystem. The important difference is that <strong>there is no root</strong>. We get data around by building, rebuilding, and passing resource graphs, rather than ACL on a general filesystem or whatever. We pass around references.
|
||||
</p>
|
||||
<h3>Programming with a resource graph</h3>
|
||||
<p>
|
||||
Today's languages are not well-suited to this model of data. Neither are computers: you can't have a pointer to an HTTP resource. Also, it needs to be enforced, so RIP native binaries. Not that you could have them anyway, since the internet runs on a loot of architectures. Instead, you'd need a bytecode interpreter that can actually handle it all natively.
|
||||
</p>
|
||||
<p>
|
||||
Also, I swear I am not a Lisp shill and I had no intention of it, but Lisp happens to be really good at dealing with linked data structures. It'd probably be really convenient for dealing with this sort of thing. Though this system is strongly typed, unlike Lisp.
|
||||
</p>
|
||||
<h3>There's more to resources than CRUD</h3>
|
||||
<p>
|
||||
There needs to be an actual way to implement all these fancy types of nodes. And how can we not care about the source of something being HTTP if we need to make a query? The solution is simple: <strong>make every node a computation</strong>. And by computation I mean closure.
|
||||
</p>
|
||||
<p>
|
||||
I mean, how did you <em>think</em> the nodes were implemented? Most nodes are actually a procedure to fetch the requested content. But you can also make nodes with inputs and outputs, such as an HTTP query. Of course, we need to know where we're getting the data from, so that must have been put in earlier. The resources with that information have been enclosed in the node.
|
||||
</p>
|
||||
<p>
|
||||
Nodes are functions. They're partially applied with a portion of the graph they require to make closures. In fact, <strong>functions are nodes too</strong>. So are all processes. You pass in a parameter graph and get back data.
|
||||
</p>
|
||||
<p>
|
||||
Now I hope it makes sense how we can have all the features of a kernel without syscalls. Your malloc or whatever is inclosed with the relevant information, including any syncronization references.
|
||||
</p>
|
||||
<h2>Step 2: Computational Economy</h2>
|
||||
<p>
|
||||
So what if we <strong>assign an expense to a function</strong>? We can count instructions, give them different expenses, and sum them up to get a final price. We can calculate the range of potential prices by calculating branches as lumps and adding them each time a branch is taken. From here, we can extend it to the cost of data (e.g. memory) by calculating <strong>quantity of data over computational time</strong>. Bandwidth costs are obvious too. This is how you can implement schedulers, when you expose the interpreter as a resource.
|
||||
</p>
|
||||
<h4>What about the halting problem?</h4>
|
||||
<p>
|
||||
Totality proofs (manual or automatic), and relating expense to the input. Where it cannot be proven, the maximum expense can be considered infinite. In many of those cases, it would make sense to put an <strong>upper bound on the amount you're willing to pay to run a function</strong>.
|
||||
</p>
|
||||
<h3>Paying for our remote access</h3>
|
||||
<p>
|
||||
Servers can also assign an expense to queries if you modified e.g. HTTP to do it. <strong>HTTP is just a kind of RPC anyway</strong>, and it now behaves exactly like one in our resource graph. Now you can pay them for your access to their resource graph!
|
||||
</p>
|
||||
<strong>We've now turned computational expense into a currency!</strong>
|
||||
<p>
|
||||
How cryptocurrencies are implemented is out of the scope of this article, but we can now turn this into one, and trade our currency for computation.
|
||||
</p>
|
||||
|
||||
But to continue, if accessing someone else's resources has a cost, we should probably be <em>paying</em> for it, right? Paying for goods and services. Seems familiar. Maybe our "money" really is just that-- a currency. Are y'all familiar with cryptocurrencies? Because we're well on our way to making one. Explaining how blockchains like bitcoin work is waay out of the scope of this post (or perhaps not-- but at any rate, it's too long to explain in this one), but to SUPER summarize it, we can use cryptographic mAgIc to sell portions of transactions and stuff with cryptographic proof, tl;dr a distributed currency. I'll have to explain how it works, and how you can make contracts to prevent scams and stuff, and how to deal with redundant computation in a different post, because you have no idea just how much further I can push this (i.e. I don't have time for that sort of digression).
|
||||
|
||||
The end result is that your pair of computers can trade resources and do all sorts of crazy stuff all beneath the nose of the program itself. This can be generalized to a more sensible system by decoupling the e.g. local per-instruction expense and currency to allow competition between suppliers, but that's pretty complicated too, and I want to stick to the realm of abstractions, rather than defining the economic system. Anyway, from there you can just extend this abstraction over an entire network of computers, and buy/sell resources as needed. You're probably seeing a lot of issues at this point (e.g. what if the other computers lie, what if they drop my data, what about latency, what about network partitions, what if they steal my data, how do I deal with all of these transactions in a performant matter), but don't worry, I'll get to them later. Actually, there are going to be a /lot/ of places coming up where I'll have to get to it later, so I'm going to stop giving this notice, but I will cover them. Also, if you're thinking, "this keeps sounding less and less like osdev", you're right. I'm no longer strictly discussing operating systems-- I've generalized the concept of an operating system, which abstracts over hardware and other such things, to an entire network.
|
||||
|
||||
Now that's a pretty big claim, but none of what I've said so far is all that impressive. Most of us have enough power on our computers not to need to buy it, and just doing these tasks the old-fashioned way is a heck of a lot easier for these benefits so far (though before I got so far out, the ideas still in the realm of typical operating systems is more justification than a lot of hobby OSes). The thing is, I'm claiming to abstract over the internet, but really all I've talked about is loaning resources and paying for data. Applications haven't changed that much, only their execution platform, and a couple of conveniences. For example, your HTTP server still holds all your data, you're just getting paid for holding it (though you can pay other people to act like a CDN). The issue is that while the computation is distributed and that space can be loaned, data is still fundamentally centralized. Sure, it's over a bunch of computers, but there's no concept of shared data. Your applications can run all <em>over</em> the internet, but not <em>on</em> it.
|
||||
|
||||
<h2>Running <em>ON</em> the Internet -- Fully distributed applications</h2>
|
||||
Now we're finally at my point. What I want is to be able to write fully distributed multi-user applications in a similar way to how we write standard applications now. There shouldn't be a server or host or central authority, you shouldn't have to deal with figuring out where data is stored, you shouldn't have to figure out the fine details of protocols, and such things. Publishing pages or files Web 1.0-style shouldn't require any hosting, and <em>all</em> data should receive the benefits of torrenting automatically. Interactive content (web 2.0, IRC, etc) should behave similarly. Games shouldn't need to worry about hosting (all multiplayer games should be as easy as LAN hosting is today, and large servers should be a hell of a lot cheaper i.e. free). A distributed data store.
|
||||
|
||||
<h2>Getting back to details</h2>
|
||||
If you can't think of a billion potential issues with this, I'm disappointed in you. But don't worry, I've reached peak abstraction, and now I can start working my way back down into details and issues. I'm probably going to go from easier issues to harder issues and low-level issues to high-level issues, just fyi. I know this is written like an FAQ but I keep building on important details here.
|
||||
|
||||
* Aren't interpreters slow? How is it a good idea to run your entire operating system on them?
|
||||
They are typically slow, but as they're the core of the entire everything, a lot of optimization would go into it. It'd probably be rather low-level bytecode, and have an extremely efficient interpreter. Some degree of JITting would probably occur, when there is very high confidence it won't open up a bug. Since resources are managed in a graph and implicit dependencies are impossible, I'd assume people could take advantage of these properties to achieve an extremely high level of parallelism, like they do in functional programming languages.
|
||||
|
||||
* How would it be safe to run unknown code on your computer?
|
||||
It's not, but you're probably doing it right now with your browser. There's the obvious distinction between going to trusted websites and getting pushed data from strangers, though. There's some inevitable risk in any internet connection, and the best you can do is minimize that risk. I would try to keep the inner interpreter extremely simple and small, perhaps even going as far as to formally verify it, to prevent exploits; JITting should be used with extreme caution; I would sandbox processes pushed to me when possible; and I would also try to take the precautions used by OSes such as OpenBSD. Overall though, I'm reasonably confident in it, and the complete lack of implicit dependencies makes it a hell of a lot more secure than running random executables, even sandboxed ones, and brings it closer to e.g. JS. The language wouldn't even deal with numeric pointers (to real memory, not as in the concept), to prevent accidental pointer arithmetic bugs.
|
||||
|
||||
<h4>How do I access raw resources from the interpreted language?</h4>
|
||||
The interpreter would pass in operations for raw resource access into the boot program, which can then create closures wrapping these resources (e.g. a memory allocator, a partition reader, other device wrappers) and keep building abstractions on these, with only the abstractions being included in the resource graph for normal programs. How these raw resources are provided is an implementation detail. It could potentially involve bootstrap stages and assembly output.
|
||||
|
||||
<h4>Okay, well how do these abstractions work? <strong>What is a graph node anyhow?</strong></h4>
|
||||
Each node is essentially a function call, though most of the actual function calls would be optimized away. You pass in a graph with the correct data types, and assign the result to another local graph node. The closures are actually more like partially applied functions in this sense, since the graph has to be explicitly passed in and must have exactly the required functions and nothing more, but I call them closures because it "captures" the resource access primitives from the creator, and then gets given actual input later. Resources like an HTTP call are essentially just lazily-evaluated procedures.
|
||||
|
||||
<h4>How is it performant to have a program distributed over multiple computers? <strong>How does the network manage latency and throughput?</strong></h4>
|
||||
Usually, it isn't. Loaning resources isn't the point, it's just a necessary abstraction to build the rest of the network, for things like contracts, and managing the distributed data store. Usually, the actual computation and its related data will be transferred as a block (lazily, of course) to the actual place of execution, and only independent batch jobs will be transferred. A computer would rarely actually pay for a computation unless necessary (think swap space), and will do computations locally when possible, and local-initiated computations always take priority over sold computations. There are only two purposes other than for internal infrastructure and massively distributed computation projects: conserving battery life, and accessing remote resources. Often it doesn't make sense to download large portions of a database when the content you actually want is a lot smaller, so you just pay someone who already has it to do it for you. If this is a common case and it gets overwhelmed, its own price goes up until someone else finds it cheaper to grab the data than pay for it, and then you have two cheap servers. They don't have to maintain a clone of the database obviously, but in most cases, for a commonly-accessed resource, it makes sense because you can resell (seed) the data yourself, or you'll want to retrieve it again and have it there. This is how static (as opposed to stateful, not dynamic) data propagates through the network. You can tell whether something is common by announcing you have it, and holding onto it. This means that the more popular a resource is, the faster and cheaper it becomes to retrieve because more people have it. If it becomes less popular, or otherwise overhosted, people will automatically drop it because it's no longer profitable to host. Additionally, the more people host something, the more likely there is a version close to you, which reduces latency. This is especially true of geographically popular data. Beyond that, it is trivial to chunk data, so that the end users receive <strong>all data like a bittorrent</strong>. Through these mechanisms, <strong>static data would be much faster than the normal internet, since all data behaves like a torrent or CDN.</strong> Stateful data still receives many of these benefits, but that'll have to wait for later.
|
||||
|
||||
I had to take a break from writing this post, so hopefully I don't miss anything. I probably will, having lost my train of thought now.
|
||||
|
||||
* Isn't it expensive to track computations like that / CPU cache & branch prediction?
|
||||
You can calculate the length of each block in advance, and only need to add the sum of the block to the total when a branch is taken. Locally initiated code could under some circumstances be free and not need to be tracked at all.
|
||||
|
||||
* Can this have any <em>benefit</em> to security, as far as local programs go?
|
||||
Isolation of programs & capability-based security: no implicit dependencies or global resource graph to exploit. You can't traverse e.g. the whole filesystem because the concept of "the whole filesystem" isn't meaningful.
|
||||
|
||||
<h2>The implementation of distributed state</h2>
|
||||
Oh lord. Now I have to move onto the implementation of distributed state. I'm not really looking forward to this, since everything I've said so far is just the tip of the iceberg as far as details go. Most of my countless pages of notebook are trying to work around the insane difficulties of building a general case for distributed applications. Can't I just stick to hype? Shit. Man, and that's not even counting explaining the usual blockchain problems.
|
||||
|
||||
<h3>The guarentees of a distributed system</h3>
|
||||
What we're essentially looking at is an extremely complex internet overlay network implemented on top of the operating system I've described so far, to provide guarantees about data. We have opened the gates of hell. I suppose I should start off by listing the properties that such a network needs to be able to have:
|
||||
<ul>
|
||||
<li> The typical cryptographic guarantees: confidentiality, integrity, availability, and non-repudiation</li>
|
||||
<li> Agreement upon the order in which things occurred *with low latency* (FUCK the PACELC theorem). Sometimes a partial ordering is acceptable</li>
|
||||
<li> Prove that things actually happened to peers who did not observe it (this is incredibly complex if you don't want to use blockchain)
|
||||
</li><li> Separation of identity / pseudonymity / persistent identification: actually this is by far the easiest thing here
|
||||
</li><li> The ability to locate and retrieve public data
|
||||
</li><li> Anonymity (note: I'm not willing to even think about anonymity networks. I figure this is separation of identity + layering connections over I2P or some other existing anonymity network-- I2P is just built for this sort of thing though).
|
||||
</li><li> Privacy of the data
|
||||
</li><li> Provable secrets such as e.g. player position in an FPS
|
||||
</li><li> Reforming the network in the case of a partition
|
||||
</li><li> The ability to update the program while maintaining the same data store
|
||||
</li><li> Guaranteeing consistent data across the entire network
|
||||
</li><li> Preventing lying about data
|
||||
</li><li> Separation of semantic units of data-- only perform necessary replication of calculations, and only providing the guarantees necessary for a particular block of data
|
||||
</li><li> Resilience against censorship, malicious firewalls, DDOS, and such
|
||||
</li><li> Continued functionality in high-latency and/or low-bandwidth environments, and unreliable connections
|
||||
</li><li> Protection against <em>spam</em> and cheaters
|
||||
</li><li> Multi-modality for when server architectures just work best for performance
|
||||
</li><li> Prevention against data loss, especially for the ability to do stuff like long-term remote file hosting
|
||||
</li><li> Plausible deniability</li>
|
||||
</ul>
|
||||
</article>
|
||||
<footer>
|
||||
<div class="license"><a rel="license" href="http://creativecommons.org/licenses/by-sa/4.0/"><img alt="Creative Commons License" style="border-width:0" src="/res/cc-by-sa-small.png" /></a> This work is licensed under a <a rel="license" href="http://creativecommons.org/licenses/by-sa/4.0/">Creative Commons Attribution-ShareAlike 4.0 International License</a>.</div>
|
||||
<div>Open Iconic — <a href="https://www.useiconic.come/open">www.useiconic.com/open</a> / MIT Licensed, attribution optional</div>
|
||||
<div>This page is friendly to text browsers.</div>
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -0,0 +1 @@
|
|||
Test content
|
||||
Binary file not shown.
|
|
@ -39,9 +39,6 @@
|
|||
<div id="navbrand">Lijero</div>
|
||||
<ul>
|
||||
<li><a href="/">Home</a></li>
|
||||
<li>Music</li>
|
||||
<li>Games</li>
|
||||
<li>About</li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
|
|
@ -75,3 +72,4 @@ but this often comes at the cost of readability. My goal with this website is to
|
|||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
|
||||
|
|
@ -0,0 +1,25 @@
|
|||
<!DOCTYPE html>
|
||||
<html>
|
||||
<head>
|
||||
<title>Welcome to nginx!</title>
|
||||
<style>
|
||||
body {
|
||||
width: 35em;
|
||||
margin: 0 auto;
|
||||
font-family: Tahoma, Verdana, Arial, sans-serif;
|
||||
}
|
||||
</style>
|
||||
</head>
|
||||
<body>
|
||||
<h1>Welcome to nginx!</h1>
|
||||
<p>If you see this page, the nginx web server is successfully installed and
|
||||
working. Further configuration is required.</p>
|
||||
|
||||
<p>For online documentation and support please refer to
|
||||
<a href="http://nginx.org/">nginx.org</a>.<br/>
|
||||
Commercial support is available at
|
||||
<a href="http://nginx.com/">nginx.com</a>.</p>
|
||||
|
||||
<p><em>Thank you for using nginx.</em></p>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -17,6 +17,8 @@
|
|||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<meta http-equiv="refresh" content="5; url=https://lijero.co/switte/" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
|
|
@ -36,39 +38,15 @@
|
|||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<div id="navbrand">Lijero</div>
|
||||
<ul>
|
||||
<li><a href="/">Home</a></li>
|
||||
</ul>
|
||||
<span id="navbrand">Lijero</span>
|
||||
</nav>
|
||||
<article>
|
||||
<header>
|
||||
<h1>Test Content</h1>
|
||||
<h1>Home Page</h1>
|
||||
</header>
|
||||
<h2>Summary</h2>
|
||||
<div class="aside quote">
|
||||
<div class="quote-content"> To make an apple pie from scratch, you must first invent the universe. </div>
|
||||
<div class="author">~ Carl Sagan</div>
|
||||
</div>
|
||||
<p>
|
||||
This is some <a href="//example.com">test content</a>. The purpose of this content is to demonstrate the readability of small-width, large-margined, well-spaced, large text. A lot of websites are extremely compact,
|
||||
but this often comes at the cost of readability. My goal with this website is to provide an entirely different and more attractive user experience.
|
||||
</p>
|
||||
<h2>Lorem Ipsum</h2>
|
||||
<p>Pellentesque habitant morbi tristique senectus et netus et malesuada fames ac turpis egestas. Vestibulum tortor quam, feugiat vitae, ultricies eget, tempor sit amet, ante. Donec eu libero sit amet quam egestas semper. Aenean ultricies mi vitae est. Mauris placerat eleifend leo. Quisque sit amet est et sapien ullamcorper pharetra. Vestibulum erat wisi, condimentum sed, commodo vitae, ornare sit amet, wisi. Aenean fermentum, elit eget tincidunt condimentum, eros ipsum rutrum orci, sagittis tempus lacus enim ac dui. Donec non enim in turpis pulvinar facilisis. Ut felis. Praesent dapibus, neque id cursus faucibus, tortor neque egestas augue, eu vulputate magna eros eu erat. Aliquam erat volutpat. Nam dui mi, tincidunt quis, accumsan porttitor, facilisis luctus, metus</p>
|
||||
<h2>Extra Content</h2>
|
||||
<p>I have a bunch of content already, but I think a third paragraph would be nice too. In addition, this lets me intract with the website through scrolling, which could possibly make a difference, though I can't say for sure. Anyway, this content should help with both of these issues.</p>
|
||||
<p>Sorry! This site is under construction.</p>
|
||||
<p>In the mean time, here's a redirect to <a href="/switte/">the Switte Programming Language</a></p>
|
||||
</article>
|
||||
<footer>
|
||||
<div class="metadata">
|
||||
<span><img alt="Author" src="//lijero.co/res/icon/person.svg" /> Lijero</span>
|
||||
<span><img alt="Updated" src="//lijero.co/res/icon/clock.svg" /> 2017-12-16</span>
|
||||
<div class="license">
|
||||
<a rel="license" href="http://creativecommons.org/licenses/by-sa/4.0/">
|
||||
<img alt="This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License" style="border-width:0" src="/res/cc-by-sa-small.png" />
|
||||
</a>
|
||||
</div>
|
||||
</div>
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
|
||||
|
|
|
|||
|
|
@ -1,79 +0,0 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<!-- Uses Open Iconic: MIT licenses, attribution optional licenses. -->
|
||||
<!-- This page is friendly to text browsers. -->
|
||||
<head>
|
||||
<meta charset="utf-8" />
|
||||
|
||||
<meta name="author" content="Lijero" />
|
||||
<!-- <meta name="description" content="" /> -->
|
||||
<meta name="keywords" content="Lijero,music,code,producer,games,website" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>Lijero</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
_paq.push(["setDocumentTitle", document.domain + "/" + document.title]);
|
||||
_paq.push(["setCookieDomain", "*.lijero.co"]);
|
||||
_paq.push(["setDomains", ["*.lijero.co"]]);
|
||||
_paq.push(['trackPageView']);
|
||||
_paq.push(['enableLinkTracking']);
|
||||
(function() {
|
||||
var u="//p.lijero.co/";
|
||||
_paq.push(['setTrackerUrl', u+'foo']);
|
||||
_paq.push(['setSiteId', '1']);
|
||||
var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];
|
||||
g.type='text/javascript'; g.async=true; g.defer=true; g.src=u+'foo.js'; s.parentNode.insertBefore(g,s);
|
||||
})();
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<div id="navbrand">Lijero</div>
|
||||
<ul>
|
||||
<li><a href="/">Home</a></li>
|
||||
<li>Music</li>
|
||||
<li>Games</li>
|
||||
<li>About</li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
<header>
|
||||
<h1>Test Content</h1>
|
||||
</header>
|
||||
<h2>Summary</h2>
|
||||
<div class="aside quote">
|
||||
<div class="quote-content"> To make an apple pie from scratch, you must first invent the universe. </div>
|
||||
<div class="author">~ Carl Sagan</div>
|
||||
</div>
|
||||
<p>NOTICE: I have some real content located at <a href="https://lijero.co/articles/beyond-operating-systems">Beyond Operating Systems</a>, though it is heavily WIP.
|
||||
</p>
|
||||
<p>
|
||||
This is some <a href="//example.com">test content</a>. The purpose of this content is to demonstrate the readability of small-width, large-margined, well-spaced, large text. A lot of websites are extremely compact,
|
||||
but this often comes at the cost of readability. My goal with this website is to provide an entirely different and more attractive user experience.
|
||||
</p>
|
||||
<h2>Lorem Ipsum</h2>
|
||||
<p>Pellentesque habitant morbi tristique senectus et netus et malesuada fames ac turpis egestas. Vestibulum tortor quam, feugiat vitae, ultricies eget, tempor sit amet, ante. Donec eu libero sit amet quam egestas semper. Aenean ultricies mi vitae est. Mauris placerat eleifend leo. Quisque sit amet est et sapien ullamcorper pharetra. Vestibulum erat wisi, condimentum sed, commodo vitae, ornare sit amet, wisi. Aenean fermentum, elit eget tincidunt condimentum, eros ipsum rutrum orci, sagittis tempus lacus enim ac dui. Donec non enim in turpis pulvinar facilisis. Ut felis. Praesent dapibus, neque id cursus faucibus, tortor neque egestas augue, eu vulputate magna eros eu erat. Aliquam erat volutpat. Nam dui mi, tincidunt quis, accumsan porttitor, facilisis luctus, metus</p>
|
||||
<h2>Extra Content</h2>
|
||||
<p>I have a bunch of content already, but I think a third paragraph would be nice too. In addition, this lets me intract with the website through scrolling, which could possibly make a difference, though I can't say for sure. Anyway, this content should help with both of these issues.</p>
|
||||
</article>
|
||||
<footer>
|
||||
<div class="metadata">
|
||||
<span><img alt="Author" src="//lijero.co/res/icon/person.svg" /> Lijero</span>
|
||||
<span><img alt="Updated" src="//lijero.co/res/icon/clock.svg" /> 2017-12-16</span>
|
||||
<div class="license">
|
||||
<a rel="license" href="http://creativecommons.org/licenses/by-sa/4.0/">
|
||||
<img alt="This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License" style="border-width:0" src="/res/cc-by-sa-small.png" />
|
||||
</a>
|
||||
</div>
|
||||
</div>
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -6,14 +6,17 @@
|
|||
<meta charset="utf-8" />
|
||||
|
||||
<meta name="author" content="Lijero" />
|
||||
<!-- <meta name="description" content="" /> -->
|
||||
<meta name="keywords" content="Lijero,music,code,producer,games,website" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>Lijero - Projects</title>
|
||||
<title>Lijero</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
|
|
@ -33,31 +36,14 @@
|
|||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<div id="navbrand">Lijero</div>
|
||||
<ul>
|
||||
<li><a href="/">Home</a></li>
|
||||
</ul>
|
||||
<span id="navbrand">Lijero</span>
|
||||
</nav>
|
||||
<article>
|
||||
<header>
|
||||
<h1>Projects</h1>
|
||||
<h1>Home Page</h1>
|
||||
</header>
|
||||
<h2>Current Projects</h2>
|
||||
<h3>The Switte Programming Language</h3>
|
||||
<p>A programming language based on context-sensitive grammar production rules, derived from ordered linear dependent type theory.</p>
|
||||
<h3>Switte Rules</h3>
|
||||
<p>A rule processing engine + transactional database.</p>
|
||||
<h2>Planned projects</h2>
|
||||
<h3>SwitteOS</h3>
|
||||
<p>An operating system based on the Switte programming language.</p>
|
||||
<h3>SwitteNet</h3>
|
||||
<p>A distributed overlay network.</p>
|
||||
<p>Sorry! This site is under construction. It should be up by the end of March, so consider checking back then.</p>
|
||||
</article>
|
||||
<footer>
|
||||
<div class="metadata">
|
||||
<span><img alt="Author" src="//lijero.co/res/icon/person.svg" /> Lijero</span>
|
||||
<span><img alt="Updated" src="//lijero.co/res/icon/clock.svg" /> 2018-01-19</span>
|
||||
</div>
|
||||
</footer>
|
||||
</body>
|
||||
</html>
|
||||
|
||||
|
|
@ -0,0 +1,88 @@
|
|||
server {
|
||||
listen 80 default_server;
|
||||
listen [::]:80 default_server;
|
||||
|
||||
server_name _;
|
||||
|
||||
location /.well-known/acme-challenge {
|
||||
try_files $uri =404;
|
||||
}
|
||||
|
||||
return 301 https://$host$request_uri;
|
||||
}
|
||||
|
||||
server {
|
||||
listen 443 ssl http2 default_server;
|
||||
listen [::]:443 ssl http2 default_server;
|
||||
|
||||
ssl on;
|
||||
|
||||
ssl_certificate /etc/letsencrypt/live-ecdsa/lijero.co/chain.pem;
|
||||
ssl_certificate_key /etc/letsencrypt/live-ecdsa/lijero.co/privkey.pem;
|
||||
ssl_session_timeout 1d;
|
||||
ssl_session_cache shared:SSL:50m;
|
||||
ssl_session_tickets off;
|
||||
|
||||
ssl_protocols TLSv1.2;
|
||||
# ssl_protocols TLSv1.2 TLSv1.3;
|
||||
ssl_ciphers 'ECDHE-ECDSA-CHACHA20-POLY1305:ECDHE-ECDSA-AES256-GCM-SHA384:ECDHE-ECDSA-AES256-SHA384:ECDHE-ECDSA-AES256-SHA384:ECDHE-ECDSA-AES256-SHA:ECDHE-ECDSA-AES128-GCM-SHA256';
|
||||
ssl_prefer_server_ciphers on;
|
||||
|
||||
ssl_ecdh_curve secp384r1:secp521r1;
|
||||
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
|
||||
ssl_stapling on;
|
||||
ssl_stapling_verify on;
|
||||
|
||||
resolver 192.168.1.1;
|
||||
# resolver 8.8.4.4;
|
||||
|
||||
ssl_trusted_certificate /etc/letsencrypt/live-ecdsa/lijero.co/chain.pem;
|
||||
|
||||
root /var/www/html;
|
||||
|
||||
index index.xhtml;
|
||||
|
||||
server_name _;
|
||||
|
||||
#add_header Content-Security-Policy "default-src 'none'; image-src 'self'; style-src 'self';";
|
||||
|
||||
location / {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
add_header Link "</res/common.css>; rel=preload; as=style;";
|
||||
try_files $uri $uri/ =404;
|
||||
gzip on;
|
||||
}
|
||||
|
||||
location /res/ {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
# expires 7d;
|
||||
# add_header Cache-Control "public";
|
||||
gzip on;
|
||||
}
|
||||
|
||||
location /res/cc-by-sa-small.png {
|
||||
expires 180d;
|
||||
}
|
||||
|
||||
location /res/icon/ {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
expires 30d;
|
||||
gzip on;
|
||||
add_header Cache-Control "public";
|
||||
}
|
||||
|
||||
location /favicon.png {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
add_header Cache-Control "public";
|
||||
expires 60d;
|
||||
gzip on;
|
||||
}
|
||||
|
||||
location ~ \.php$ {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
include snippets/fastcgi-php.conf;
|
||||
fastcgi_pass unix:/var/run/php/php7.0-fpm.sock;
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,88 @@
|
|||
server {
|
||||
listen 80 default_server;
|
||||
listen [::]:80 default_server;
|
||||
|
||||
server_name _;
|
||||
|
||||
location /.well-known/acme-challenge {
|
||||
try_files $uri =404;
|
||||
}
|
||||
|
||||
return 301 https://$host$request_uri;
|
||||
}
|
||||
|
||||
server {
|
||||
listen 443 ssl http2 default_server;
|
||||
listen [::]:443 ssl http2 default_server;
|
||||
|
||||
ssl on;
|
||||
|
||||
ssl_certificate /etc/letsencrypt/live-ecdsa/lijero.co/chain.pem;
|
||||
ssl_certificate_key /etc/letsencrypt/live-ecdsa/lijero.co/privkey.pem;
|
||||
ssl_session_timeout 1d;
|
||||
ssl_session_cache shared:SSL:50m;
|
||||
ssl_session_tickets off;
|
||||
|
||||
ssl_protocols TLSv1.2;
|
||||
# ssl_protocols TLSv1.2 TLSv1.3;
|
||||
ssl_ciphers 'ECDHE-ECDSA-CHACHA20-POLY1305:ECDHE-ECDSA-AES256-GCM-SHA384:ECDHE-ECDSA-AES256-SHA384:ECDHE-ECDSA-AES256-SHA384:ECDHE-ECDSA-AES256-SHA:ECDHE-ECDSA-AES128-GCM-SHA256';
|
||||
ssl_prefer_server_ciphers on;
|
||||
|
||||
ssl_ecdh_curve secp384r1:secp521r1;
|
||||
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
|
||||
ssl_stapling on;
|
||||
ssl_stapling_verify on;
|
||||
|
||||
resolver 192.168.1.1;
|
||||
# resolver 8.8.4.4;
|
||||
|
||||
ssl_trusted_certificate /etc/letsencrypt/live-ecdsa/lijero.co/chain.pem;
|
||||
|
||||
root /var/www/html;
|
||||
|
||||
index index.xhtml;
|
||||
|
||||
server_name _;
|
||||
|
||||
#add_header Content-Security-Policy "default-src 'none'; image-src 'self'; style-src 'self';";
|
||||
|
||||
location / {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
add_header Link "</res/common.css>; rel=preload; as=style;";
|
||||
try_files $uri $uri/ =404;
|
||||
gzip on;
|
||||
}
|
||||
|
||||
location /res/ {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
# expires 7d;
|
||||
# add_header Cache-Control "public";
|
||||
gzip on;
|
||||
}
|
||||
|
||||
location /res/cc-by-sa-small.png {
|
||||
expires 180d;
|
||||
}
|
||||
|
||||
location /res/icon/ {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
expires 30d;
|
||||
gzip on;
|
||||
add_header Cache-Control "public";
|
||||
}
|
||||
|
||||
location /favicon.png {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
add_header Cache-Control "public";
|
||||
expires 60d;
|
||||
gzip on;
|
||||
}
|
||||
|
||||
location ~ \.php$ {
|
||||
add_header Strict-Transport-Security "max-age=15768000; includeSubDomains; preload";
|
||||
include snippets/fastcgi-php.conf;
|
||||
fastcgi_pass unix:/var/run/php/php7.0-fpm.sock;
|
||||
}
|
||||
}
|
||||
|
|
@ -136,3 +136,8 @@ nav li {
|
|||
margin-left: -20px;
|
||||
}
|
||||
}
|
||||
|
||||
pre {
|
||||
font-size: 16px;
|
||||
padding-left: 2em;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -18,6 +18,10 @@ nav {
|
|||
font-style: italic;
|
||||
}
|
||||
|
||||
nav li {
|
||||
text-indent: 0;
|
||||
}
|
||||
|
||||
nav ul {
|
||||
list-style: none;
|
||||
}
|
||||
|
|
@ -33,7 +37,7 @@ article {
|
|||
p {
|
||||
/* text-align: justify;
|
||||
text-justify: distribute;*/
|
||||
text-indent: 4em;
|
||||
text-indent: 2em;
|
||||
}
|
||||
|
||||
article h1 {
|
||||
|
|
@ -106,66 +110,29 @@ footer {
|
|||
}
|
||||
}
|
||||
|
||||
@media screen and (max-width: 1200px) {
|
||||
nav {
|
||||
margin: auto;
|
||||
padding: 0;
|
||||
text-align: center;
|
||||
}
|
||||
nav {
|
||||
margin: auto;
|
||||
padding: 0;
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
nav ul {
|
||||
padding: 0;
|
||||
}
|
||||
nav ul {
|
||||
padding: 0;
|
||||
}
|
||||
|
||||
nav li {
|
||||
margin: 0;
|
||||
display: inline-block;
|
||||
}
|
||||
nav li {
|
||||
margin: 0;
|
||||
display: inline-block;
|
||||
}
|
||||
|
||||
@media screen and (min-width: 700px) {
|
||||
article {
|
||||
padding: 30px 80px;
|
||||
padding: 0 80px;
|
||||
min-width: 25em;
|
||||
max-width: 30em;
|
||||
max-width: 33em;
|
||||
}
|
||||
|
||||
article h1 {
|
||||
margin-left: -20px;
|
||||
}
|
||||
}
|
||||
|
||||
@media screen and (min-width: 1200px) {
|
||||
nav {
|
||||
max-width: 15%;
|
||||
float: left;
|
||||
padding: 20px 45px 40px 40px;
|
||||
margin-top: 10px;
|
||||
border-right: 3px solid;
|
||||
}
|
||||
|
||||
nav span {
|
||||
padding-left: 20px;
|
||||
}
|
||||
|
||||
nav ul {
|
||||
margin-left: 20px;
|
||||
}
|
||||
|
||||
nav li {
|
||||
border-bottom: 1px solid #ccc;
|
||||
padding: 3px;
|
||||
}
|
||||
|
||||
nav ul li:last-child {
|
||||
border-bottom: none;
|
||||
}
|
||||
|
||||
.aside {
|
||||
position: relative;
|
||||
left: 60%;
|
||||
float: right;
|
||||
margin-left: -50%;
|
||||
max-width: 50%;
|
||||
}
|
||||
}
|
||||
BIN
resume.docx
BIN
resume.docx
Binary file not shown.
BIN
resume.odt
BIN
resume.odt
Binary file not shown.
Binary file not shown.
|
|
@ -0,0 +1,145 @@
|
|||
\documentclass[11pt]{article}
|
||||
\usepackage{enumitem}
|
||||
\usepackage{hyperref}
|
||||
\usepackage[compact]{titlesec}
|
||||
|
||||
\renewcommand{\familydefault}{\sfdefault}
|
||||
|
||||
\topmargin=0.0in %length of margin at the top of the page (1 inch added by default)
|
||||
\oddsidemargin=0.0in %length of margin on sides for odd pages
|
||||
\evensidemargin=0in %length of margin on sides for even pages
|
||||
\textwidth=6.5in %How wide you want your text to be
|
||||
\marginparwidth=0.5in
|
||||
\headheight=0pt %1in margins at top and bottom (1 inch is added to this value by default)
|
||||
\headsep=0pt %Increase to increase white space in between headers and the top of the page
|
||||
\textheight=9.0in %How tall the text body is allowed to be on each page
|
||||
|
||||
\setcounter{secnumdepth}{0}
|
||||
\setlength{\parindent}{0pt}
|
||||
\setlength{\topmargin}{1pt}
|
||||
|
||||
\addtolength{\textwidth}{2cm}
|
||||
\addtolength{\hoffset}{-1cm}
|
||||
\addtolength{\textheight}{2cm}
|
||||
\addtolength{\voffset}{-1cm}
|
||||
|
||||
\begin{document}
|
||||
\centerline{\LARGE James Martin}
|
||||
\centerline{Renton, WA 98056 | \href{mailto:jtmar@lijero.co}{jtmar@lijero.co} | 206-660-7633}
|
||||
\centerline{\href{https://lijero.co/}{Website} | \href{https://github.com/lijerom/}{GitHub} | \href{https://www.linkedin.com/in/jtmarlijero/}{LinkedIn}}
|
||||
|
||||
\section{Capabilities}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Model complex real-world problems} in a way conducive to long-term growth
|
||||
\item {\bf Simplify code} and {\bf waste less time} with powerful, reusable, understandable, DRY abstractions
|
||||
\item {\bf Squash bugs} with sustainable design, clean code, unit testing, and test-driven development
|
||||
\item {\bf Maximize productivity} by taking advantage of build tools, continuous integration, bugtrackers, development environments, and version control
|
||||
\item {\bf Quick understanding} and {\bf deep conceptual connections} from a thorough theoretical background
|
||||
\item {\bf Read and write specifications} to communicate formal details clearly and understand terse descriptions
|
||||
\end{itemize}
|
||||
|
||||
\section{Programming}
|
||||
\subsubsection{Technical Skills}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Languages}: Java, C\#, C, Forth, x86 assembly, Rust, Haskell, Scheme (Lisp), Prolog, SQL, HTML, CSS
|
||||
\item {\bf Tools}: Git, Haskell's Stack, Java's Gradle, Visual Studio, Eclipse, Emacs
|
||||
\item {\bf Bug squashing}: JUnit, QuickCheck, Jenkins CI, Travis CI, GitHub issues, and more
|
||||
\item {\bf Documents}: Microsoft Office (incl. Word, Excel, PowerPoint), \LaTeX
|
||||
\end{itemize}
|
||||
|
||||
\subsubsection{Domain-Oriented Knowledge}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Exploit parallel problems} with multithreaded processes and distributed networks
|
||||
\item {\bf Solve optimization and learning problems} through neural networks, evolutionary algorithms, and logic/constraint programming
|
||||
\item {\bf Improve program and data structuring} with a powerful grasp of dataflow programming and complex control flow, including FRP, continuations, and laziness
|
||||
\item {\bf Get the most out of your language} with metaprogramming, macros, reflection, and generics
|
||||
\end{itemize}
|
||||
|
||||
\section{Systems}
|
||||
\subsubsection{Server Skills}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Daemons}: Nginx, Bind9 (authoritative), OpenSSH (SSH, SFTP), MariaDB
|
||||
\item {\bf HTTP}: Caching (client-side \& server-side), CDNs, semantic URLs, REST
|
||||
\item {\bf TLS \& Certs}: \href{https://www.ssllabs.com/ssltest/analyze.html?d=lijero.co\&latest}{A+ rating on SSLLabs}, ECDHE, RSA, Let's Encrypt, DNS CAA, OCSP, HSTS
|
||||
\item {\bf Administration}: VPSes, firewalls (incl. iptables), capability-based security, disk encryption
|
||||
\item {\bf Operating Systems}: Linux (esp. Debian, desktop \& server), Windows (XP, 7, 8)
|
||||
\end{itemize}
|
||||
|
||||
\subsubsection{Protocols}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Can write packets by hand}: HTTP, IRC, SMTP, FTP
|
||||
\item {\bf Implemented}: HTTP, IRC, Minecraft Protocol, and protocols I have made myself
|
||||
\item {\bf Very familiar}: IP, TCP, UDP, TLS/SSL, HTTP/2
|
||||
\end{itemize}
|
||||
|
||||
\section{Major Projects}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Games}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Minecraft clone}, written in C\# using the Unity game engine
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Procedural content generation} using Simplex noise
|
||||
\item {\bf Networked multiplayer} mostly implemented
|
||||
\item {\bf Hand-written mesh generation} and optimization
|
||||
\item Map editing and world save files
|
||||
\end{itemize}
|
||||
\item {\bf Minecraft server implementation} in Rust, but not enough to be usable for gameplay
|
||||
\item {\bf Mario-like platformer} game with a map editor and saving
|
||||
\item Familar with the {\bf modern OpenGL} graphics pipeline and {\bf GLSL shaders}, but not yet in practice
|
||||
\end{itemize}
|
||||
\item {\bf Low-level}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Operating system}: Kernel, memory manager, filesystem, BIOS terminal IO, paging
|
||||
\item {\bf Minecraft redstone CPU}: 16-bit stack-based von-neumann, before command blocks were added
|
||||
\item {\bf Instruction set and CPU design}, though it was never physically built
|
||||
\end{itemize}
|
||||
\item {\bf Language Extensions}: The {\bf reactive paradigm}, an {\bf event system}, and a {\bf component-based object system}, for Java using reflection
|
||||
\item {\bf Programming Language Implementations}: Dozens of {\bf Lisp}s, {\bf Forth} (x86 asm), and {\bf Prolog}
|
||||
\item {\bf Web}: Personal website, hierarchical discussion board, HTML/XML DSL, HTML parser in Rust
|
||||
\end{itemize}
|
||||
|
||||
\section{Education}
|
||||
\subsection{Formal}
|
||||
\subsubsection{2015 - Present | Hazen High School}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item Multiple college-level and honors courses, including AP Computer Science
|
||||
\item Straight-As last semester
|
||||
\end{itemize}
|
||||
|
||||
\subsection{Independent}
|
||||
In addition to previously listed skills, I have obtained:
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item Intimate familiarity with {\bf how computers function at a low level}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf CPU design and implementation}
|
||||
\item {\bf Operating systems}: Kernels, memory management, scheduling, paging, syscalls, filesystems, network stacks, BIOS/UEFI, bootloaders
|
||||
\end{itemize}
|
||||
\item {\bf Deep understanding of programming languages}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item {\bf Programming language theory} explains the implementation of programming language
|
||||
\item {\bf Type theory} (polymorphic, dependent, linear, noncommutative) is the logic and structure
|
||||
\item {\bf Category Theory} is the theoretical background to abstractions
|
||||
\item {\bf Formal languages \& semantics} describe grammar, syntax, and behavior
|
||||
\end{itemize}
|
||||
\item {\bf Logic}: Classical logic, natural deduction, sequent calculus, lambek calculus, etc
|
||||
\item {\bf Databases}: Relational algebra, principles such as ACID, tradeoffs like CAP and PACELC
|
||||
\end{itemize}
|
||||
|
||||
\section{Experience}
|
||||
\subsubsection{2017 - Present | Java Developer | \it{Hazen Robotics Club}}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item Built {\bf foundational abstractions} that drive the entire codebase
|
||||
\item {\bf Dramatically simplified} the manual control mode by implementing a dataflow system
|
||||
\item {\bf Lead programmer} for the autonomous AI-driven mode
|
||||
\item {\bf Improved organization and productivity} by introducing and teaching Git to the team
|
||||
\end{itemize}
|
||||
|
||||
\subsubsection{2012 - 2015 | Java Developer, Admin, Owner | \it{The Mining Dead}}
|
||||
\begin{itemize}[noitemsep,nolistsep]
|
||||
\item Began at {\bf eleven years old}
|
||||
\item Managed a {\bf community of hundreds}, 60+ concurrent connections at peak hours
|
||||
\item {\bf Wrote custom functionality}, the main features of the server, with many thousands of lines of code
|
||||
\item Ran custom {\bf Linux VPS paid for by the community}
|
||||
\item Used web servers and the ``Bungee'' reverse-proxy, Technic Solder content distribution
|
||||
\end{itemize}
|
||||
\end{document}
|
||||
148
resume2.txt
148
resume2.txt
|
|
@ -1,148 +0,0 @@
|
|||
Fluent with essential programming tools:
|
||||
* I use Git or another version control system for all of my projects, and can effectively use its features, including branching and merging (https://github.com/lijerom/), also an understanding of semantic versioning
|
||||
* I have used IDEs including Visual Studio and Eclipse, and configurable editors such as Emacs
|
||||
* I know how to use command-line toolchains and manually configure project builds (GNU, Stack)
|
||||
* I can efficiently and effectively use documentation to fill holes in my knowledge when necessary
|
||||
* Familiar with continuous integration services such as Jenkins (https://ci.lijero.co)
|
||||
* Efficient reporting and management using bugtrackers such as Mantis and Github Issues
|
||||
* Microsoft Office, Word, and Excel of course! (in addition to LibreOffice)
|
||||
|
||||
Essential systems administration knowledge:
|
||||
* Windows, Linux (esp. the Debian family) on the desktop and server, FreeBSD (basic familiarity w/ use and its model)
|
||||
* Nginx (HTTP server & proxy, serves lijero.co), Bind9 (DNS, I run my own authoritative server for lijero.co), Charybdis (IRCd, formerly ran one for my friends), OpenSSHd (for myself, and formerly another two administrators), MySQL/MariaDB (basic familiarity), Murmur (mumble, formerly, for friends), FTP over SSH (I used to use it for file transfers) with my servers and VPSes
|
||||
* Use an EDCHE-384 manually generated and signed via Let's Encrypt (https://lijero.co), w/ DNS CAA, HSTS (preloaded), OCSP must staple as a certificate extension -- an A+ rating on SSLLabs -- https://www.ssllabs.com/ssltest/analyze.html?d=lijero.co&latest
|
||||
* Can configure iptables or other firewalls
|
||||
* Understand how kernels (microkernels and monolithic kernels, exokernels), filesystems, network stacks, memory managers, schedulers, thread priorities, signals, interrupts, system services, kernel modules, program loaders, swap, paging, and other such features work from my own toy operating systems! (though I've only implemented a few of these things-- a basic kernel, file system, and memory manager)
|
||||
* Basic load balancing techniques, content delivery network use, caches, semantic URLs
|
||||
* Fundamental knowledge regarding databases: basic SQL, relational algebra, ACID, transactions, CAP theorem, PACELC theorem, CRUD
|
||||
|
||||
Familiarity with essential internet protocols:
|
||||
* A basic understanding of IP and UDP, and a stronger understanding of TCP
|
||||
* I understand background behind TLS(/SSL) but not the actual protocol details (I wanted to implement TLS and TCP, but never did)
|
||||
* I have written HTTP 1.0 client libraries and servers for fun (and I understand how HTTP/2 works, though not enough to implement it)
|
||||
* HTTP interface design techniques like REST w/ JSON and XML, HTTP functions
|
||||
* Though it's not a protocol, remote procedure calls as a concept
|
||||
* An IRC client+bot from scratch capable of all basic functions
|
||||
* FTP and how it functions, as little as it's used nowadays
|
||||
and the less essential ones...
|
||||
* I wrote portions of a Minecraft server a couple years back using reverse-engineered protocol documentation, but not enough to be useful for gameplay (http://wiki.vg/Protocol)
|
||||
* I wrote internal networking functions for my own Minecraft clone using both TCP and UDP (and that's when I discovered just how unreliable UDP was!)
|
||||
* Various toy protocols I wrote, eg. a chat protocol
|
||||
|
||||
Strong theoretical background:
|
||||
* Programming language development is my main hobby
|
||||
* Firm grasp of type theory (polymorphic, dependent, linear, and non-commutative varieties-- homotopy, not so much), sequent calculus, lambek calculus
|
||||
* Firm grasp of formal logic via type theory thanks to computational trinitarianism
|
||||
* Basic background with category theory, albeit mainly through Haskell, and again, computational trinitarianism
|
||||
* Competent with functional and object-oriented abstractions and design patterns
|
||||
* In case you're running a keyword filter: YES I know recursion, loops, iteration, collections, maps (dictionaries), filtering, objects, classes, subtyping polymorphism, inheritance, interfaces, abstract classes, generics, lists, arrays, pointers, sets, multisets, stacks, trees, graphs, optionals, options, tuples, eithers, zippers, continuations (somewhat), strings, characters, integers (byte, ubyte, short, ushort, int, uint, long, ulong, bignum), decimals (float, double, bigdecimal), fixed-points, inductive types, coinductive types, lazy/eager evaluation, booleans, boolean algebra, records, unions, catamorphisms, isomorphisms, functors, monads, monoids, traversables, applicatives, foldables, semigroups, arrows, lenses, continuation-passing style, exceptions, coroutines, green threads, normal threads, mutexes, cooperative multitasking, messages, locks, atomic references, thread pools, reentrancy, thread-local storage, immutability, reference counting, garbage collection, pattern matching, category, vertical types, fixpoints, LUBs, promises, etc
|
||||
* Understand how CPUs are designed and implemented (I built a 16-bit von-neumann stack-based CPU in Minecraft, and proceeded to design a real-life one on paper, though it has never been implemented)
|
||||
* Linguistics (including artificial language construction) is another hobby of mine, and you wouldn't believe how often it comes up!
|
||||
* Formal languages and grammar in terms of production rules
|
||||
* Object-oriented, (purely) functional, imperative/procedural, reactive
|
||||
|
||||
Programming languages:
|
||||
* Java (I write most of my projects in this, Robotics club), C# (an XNA platformer a couple years back, a Minecraft clone using the Unity game engine-- most of my Java knowledge is transferrable too)
|
||||
* Haskell (used to write programming languages, parsers, and projects that don't require a lot of state or IO)
|
||||
* Racket & Chicken Scheme, dialects of Lisp, Untyped Lambda Calculus (I used it often earlier on, including a web server, XHTML/XML/SVG generation DSL, and it sat right in the core of my operating system-- lambda calculus isn't a programming language obviously but it's related-- and I still use Racket Scribble for documentation)
|
||||
* x86 assembly (used in a couple of essential components of my operating system, and used to make a Forth implementation)
|
||||
* Forth (used in conjunction with x86 assembly to bootstrap itself, as is Forth tradition, but no real programs once I had it)
|
||||
* Rust (used to write an HTML/XML parser and my Minecraft server implementation, and will likely be used again in the future)
|
||||
* (X)HTML(5), CSS, SQL, PHP (used to build a webcomic site for a friend in middle school before the project was cancelled, a basic hierarchical board called "thread", and my own (incomplete) site, though it's not very technologically impressive thanks to its deliberately minimalist design (https://lijero.co))
|
||||
* Prolog (I wrote a good chunk of an implementation of one, though I never finished, and have not used it for any real projects)
|
||||
* C (portions of the operating system, the VM for that CPU I designed but never built)
|
||||
* The yet-unnamed programming language I am building right now! (derived from non-commutative linear logic, w/ influences from Haskell, Rust, Lisp, and Forth)
|
||||
|
||||
Former projects
|
||||
===============
|
||||
|
||||
Languages
|
||||
* HTML, XML, SVG parsers and generators, DSLs
|
||||
* A dozen lisp and lambda calculus implementations (at least one in every language I've ever used)
|
||||
* An indirect-threaded Forth implementation in x86 assembly
|
||||
* Reflection-based implementation of the reactive programming paradigm for Java
|
||||
* The beginnings of a prolog implementation, never finished
|
||||
|
||||
Web
|
||||
* IRC and HTTP, clients and daemons
|
||||
* A webcomic site for a friend, until the project was cancelled
|
||||
* A heirarchical board called "thread"
|
||||
* My own minimalist website
|
||||
|
||||
Low-level
|
||||
* An operating system based on a programming language interpreter in the kernel (actually partially implemented, including the kernel, filesystem, memory manager, terminal, and the language itself), and tons of other plans for other designs that never were built
|
||||
* A 16-bit von-neumann stack-based CPU in Minecraft using pure redstone, before the age of comparators, hoppers, and command blocks
|
||||
* A CPU design for real life on paper, never implemented, and a basic virtual marchine for that CPU
|
||||
|
||||
Games
|
||||
* Tons of games in Scratch from when I was younger, too many to list
|
||||
* I owned a Minecraft server with 60+ concurrent connections at peak hours for a couple years
|
||||
- most of the content was based on custom scripts, most of which I wrote-- most vanilla content was replaced somehow, including map generation, monster spawns, the actual monsters themselves, radiation and thirst mechanics, and the beginnings of a technology mod
|
||||
- I learned through trial-and-error (mostly error) how to manage a large community of people effectively
|
||||
- this was how I really got into programming
|
||||
- used a custom modpack, distributed via a self-hosted technic solder instance
|
||||
- this is how I learnt about VPSes, and was my first introduction to Linux
|
||||
- included a network of sub-servers (the desert world, the ice world, the normal world, the vanilla desert world, a games server, a sandbox server + quest build server, and a hub) via Bungee-- though this was overkill for the server population so I went back to one server with multiple worlds
|
||||
* A Minecraft server implementation written in Rust
|
||||
- built from reverse-engineered protocol docs (http://wiki.vg/Protocol)
|
||||
- never got enough done to be useable for gameplay, but it was a cool project
|
||||
* A Minecraft clone written in C# with unity. I wrote the
|
||||
- infinite map generation with simplex noise that, if I recall correctly, I implemented myself
|
||||
- mesh generation and optimization
|
||||
- map editing capabilities
|
||||
- most of the way to networked multiplayer (partially TCP, partially UDP)
|
||||
* I've used and written various event systems and can relate them to reactive programming
|
||||
* Generic simple games like pongs, breakouts, snakes, etc
|
||||
* I have a pretty solid knowledge of OpenGL, but haven't written anything complex using it directly
|
||||
|
||||
Robotics
|
||||
* A bunch of internal abstractions for our robotics club involving basic functionality like motor controls, input mapping and configuration, and operation modes
|
||||
* A dataflow abstraction that got sidetracked into a reflection-based implementation of reactive programming for Java and then evolved into another project
|
||||
* Started work on cube recognition software, but we had a really bad season and dropped out long before it was completed
|
||||
|
||||
Current Projects
|
||||
================
|
||||
|
||||
Active
|
||||
* A programming language derived from dependent ordered linear type theory (and hopefully homotopy theory influences if I ever learn it) based on the construction of valid terms using context-sensitive grammar production rules, with an emphasis on practicality (hey, don't laugh!)
|
||||
* A rule processing engine + transactional database focused on generating, processing, and querying business data, using modern structure and a powerful rule description language
|
||||
|
||||
Planned, eventually
|
||||
* An operating system based on my programming language and category-theoretic abstractions, rather than the traditional model (I believe this will make things simpler while still being useable, hopefully)
|
||||
* A distributed overlay network for a secure, autonomous internet, and powerful abstractions for writing internet-based applications and datastores, and decentralized networks
|
||||
- the two above concepts are extremely closely intertwined with eachother and the language
|
||||
|
||||
|
||||
Real-life stuff
|
||||
===============
|
||||
|
||||
Clubs:
|
||||
* Robotics (school club)
|
||||
* Dungeons & dragons (school club)
|
||||
* Dungeons & dragons (group of friends)
|
||||
* Speech & debate (dropped out this year, definitely will do next year)
|
||||
* Marching band (class, during football season)
|
||||
* Concert band (class, the rest of the year)
|
||||
* Jazz band (0-period class before school)
|
||||
|
||||
Things I like to do:
|
||||
* Hiking & backpacking
|
||||
* Cycling (to a lesser degree)
|
||||
* Dungeons & dragons
|
||||
* Perform music
|
||||
* Listen to all sorts of music
|
||||
* Play board games or poker (for chips) & chat with friends
|
||||
* Occasional video games like Dwarf Fortress, Factorio, or Terraria with friends, formerly a LOT LOT of Minecraft
|
||||
|
||||
Hobbies:
|
||||
* Programming language theory
|
||||
* Type theory & other mathematical stuff
|
||||
* Linguistics & artificial language construction (conlanging)
|
||||
* Worldbuilding (formerly, and hopefully again someday)
|
||||
* Music theory (this one is more far off, in that I don't work with it a lot yet)
|
||||
|
||||
In summary...
|
||||
* I am fascinated by conceptual structure & expression (programming languages, human languages, mathematics, music theory, speech & debate)
|
||||
* I love creativity in structured contexts (worldbuilding, conlanging, dungeons & dragons, music theory)
|
||||
* I love music (concert band, marching band, jazz band, music theory)
|
||||
* I love nature
|
||||
BIN
resume3.docx
BIN
resume3.docx
Binary file not shown.
|
|
@ -0,0 +1,53 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charaset="utf-8" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>Community - The Switte Programming Language</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
_paq.push(["setDocumentTitle", document.domain + "/" + document.title]);
|
||||
_paq.push(["setCookieDomain", "*.lijero.co"]);
|
||||
_paq.push(["setDomains", ["*.lijero.co"]]);
|
||||
_paq.push(['trackPageView']);
|
||||
_paq.push(['enableLinkTracking']);
|
||||
(function() {
|
||||
var u="//p.lijero.co/";
|
||||
_paq.push(['setTrackerUrl', u+'foo']);
|
||||
_paq.push(['setSiteId', '1']);
|
||||
var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];
|
||||
g.type='text/javascript'; g.async=true; g.defer=true; g.src=u+'foo.js'; s.parentNode.insertBefore(g,s);
|
||||
})();
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<span id="navbrand"><a href="/switte/">Switte PL</a></span>
|
||||
<ul>
|
||||
<li><a href="/switte/download/">Download</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/docs/">Documentation</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/community/">Community</a></li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
<h2>Community</h2>
|
||||
<h3>Github: <a href="https://github.com/swittepl/switti/">swittepl/switti</a></h3>
|
||||
<p>Feel free to open an issue or pull request!</p>
|
||||
<h3>IRC Channel: <a href="http://webchat.freenode.net/?channels=%23switte">#switte IRC on freenode.net</a></h3>
|
||||
<ul>
|
||||
<li>IRC is a live chat, not customer support, so do not expect an immediate response.</li>
|
||||
<li>As-is, I am the only regular. Make sure someone's online before talking.</li>
|
||||
</ul>
|
||||
</article>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -0,0 +1,62 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charaset="utf-8" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>Community - The Switte Programming Language</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
_paq.push(["setDocumentTitle", document.domain + "/" + document.title]);
|
||||
_paq.push(["setCookieDomain", "*.lijero.co"]);
|
||||
_paq.push(["setDomains", ["*.lijero.co"]]);
|
||||
_paq.push(['trackPageView']);
|
||||
_paq.push(['enableLinkTracking']);
|
||||
(function() {
|
||||
var u="//p.lijero.co/";
|
||||
_paq.push(['setTrackerUrl', u+'foo']);
|
||||
_paq.push(['setSiteId', '1']);
|
||||
var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];
|
||||
g.type='text/javascript'; g.async=true; g.defer=true; g.src=u+'foo.js'; s.parentNode.insertBefore(g,s);
|
||||
})();
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<span id="navbrand"><a href="/switte/">Switte PL</a></span>
|
||||
<ul>
|
||||
<li><a href="/switte/download/">Download</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/docs/">Documentation</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/community/">Community</a></li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
<p>
|
||||
<strong>Switte</strong> is a programming language that uses simplicity to its advantage.
|
||||
</p>
|
||||
<pre><code>
|
||||
This is an example program.
|
||||
> ABC = mulI1 parI1 [ lemI ] map2
|
||||
</code></pre>
|
||||
<h2>Features</h2>
|
||||
<h3>Instant Relocation</h3>
|
||||
Save a program mid-execution and restart it anywhere.
|
||||
<h3>Flat Model</h3>
|
||||
Arbitrary partitions of a program are equivalent.
|
||||
Programs can safely be run out-of-order and trivially parallelized!
|
||||
<h3>Partial Evaluation</h3>
|
||||
Don't have the whole set of data all at once? That's fine!
|
||||
<h3>Complete Safety</h3>
|
||||
There's no such thing as a runtime error.
|
||||
</article>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -0,0 +1,47 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charaset="utf-8" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>The Switte Programming Language</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
_paq.push(["setDocumentTitle", document.domain + "/" + document.title]);
|
||||
_paq.push(["setCookieDomain", "*.lijero.co"]);
|
||||
_paq.push(["setDomains", ["*.lijero.co"]]);
|
||||
_paq.push(['trackPageView']);
|
||||
_paq.push(['enableLinkTracking']);
|
||||
(function() {
|
||||
var u="//p.lijero.co/";
|
||||
_paq.push(['setTrackerUrl', u+'foo']);
|
||||
_paq.push(['setSiteId', '1']);
|
||||
var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];
|
||||
g.type='text/javascript'; g.async=true; g.defer=true; g.src=u+'foo.js'; s.parentNode.insertBefore(g,s);
|
||||
})();
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<span id="navbrand"><a href="/switte/">Switte PL</a></span>
|
||||
<ul>
|
||||
<li><a href="/switte/download/">Download</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/documentation/">Documentation</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/community/">Community</a></li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
<h2>Documentation</h2>
|
||||
<p>Switte's main documentation is the specification/manual generated from the literate program Switti. Check out the <a href="/switte/download/">downloads</a>.</p>
|
||||
</article>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -0,0 +1,46 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charaset="utf-8" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>The Switte Programming Language</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
_paq.push(["setDocumentTitle", document.domain + "/" + document.title]);
|
||||
_paq.push(["setCookieDomain", "*.lijero.co"]);
|
||||
_paq.push(["setDomains", ["*.lijero.co"]]);
|
||||
_paq.push(['trackPageView']);
|
||||
_paq.push(['enableLinkTracking']);
|
||||
(function() {
|
||||
var u="//p.lijero.co/";
|
||||
_paq.push(['setTrackerUrl', u+'foo']);
|
||||
_paq.push(['setSiteId', '1']);
|
||||
var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];
|
||||
g.type='text/javascript'; g.async=true; g.defer=true; g.src=u+'foo.js'; s.parentNode.insertBefore(g,s);
|
||||
})();
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<span id="navbrand"><a href="/switte/">Switte PL</a></span>
|
||||
<ul>
|
||||
<li><a href="/switte/download/">Download</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/documentation/">Documentation</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/community/">Community</a></li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
<h2>Documentation</h2>
|
||||
</article>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -0,0 +1,49 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charaset="utf-8" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>Downloads -- The Switte Programming Language</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
_paq.push(["setDocumentTitle", document.domain + "/" + document.title]);
|
||||
_paq.push(["setCookieDomain", "*.lijero.co"]);
|
||||
_paq.push(["setDomains", ["*.lijero.co"]]);
|
||||
_paq.push(['trackPageView']);
|
||||
_paq.push(['enableLinkTracking']);
|
||||
(function() {
|
||||
var u="//p.lijero.co/";
|
||||
_paq.push(['setTrackerUrl', u+'foo']);
|
||||
_paq.push(['setSiteId', '1']);
|
||||
var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];
|
||||
g.type='text/javascript'; g.async=true; g.defer=true; g.src=u+'foo.js'; s.parentNode.insertBefore(g,s);
|
||||
})();
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<span id="navbrand"><a href="/switte/">Switte PL</a></span>
|
||||
<ul>
|
||||
<li><a href="/switte/download/">Download</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/documentation/">Documentation</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/community/">Community</a></li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
<h2>Downloads</h2>
|
||||
<p>
|
||||
There are currently no releases and no build server. However, you can build the latest code using the instructions on <a href="https://github.com/swittepl/switti">GitHub</a>.
|
||||
</p>
|
||||
</article>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -0,0 +1,62 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charaset="utf-8" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>The Switte Programming Language -- Downloads</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
_paq.push(["setDocumentTitle", document.domain + "/" + document.title]);
|
||||
_paq.push(["setCookieDomain", "*.lijero.co"]);
|
||||
_paq.push(["setDomains", ["*.lijero.co"]]);
|
||||
_paq.push(['trackPageView']);
|
||||
_paq.push(['enableLinkTracking']);
|
||||
(function() {
|
||||
var u="//p.lijero.co/";
|
||||
_paq.push(['setTrackerUrl', u+'foo']);
|
||||
_paq.push(['setSiteId', '1']);
|
||||
var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];
|
||||
g.type='text/javascript'; g.async=true; g.defer=true; g.src=u+'foo.js'; s.parentNode.insertBefore(g,s);
|
||||
})();
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<span id="navbrand"><a href="/switte/">Switte PL</a></span>
|
||||
<ul>
|
||||
<li><a href="/switte/download/">Download</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/docs/">Documentation</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/community/">Community</a></li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
<p>
|
||||
<strong>Switte</strong> is a programming language that uses simplicity to its advantage.
|
||||
</p>
|
||||
<pre><code>
|
||||
This is an example program.
|
||||
> ABC = mulI1 parI1 [ lemI ] map2
|
||||
</code></pre>
|
||||
<h2>Features</h2>
|
||||
<h3>Instant Relocation</h3>
|
||||
Save a program mid-execution and restart it anywhere.
|
||||
<h3>Flat Model</h3>
|
||||
Arbitrary partitions of a program are equivalent.
|
||||
Programs can safely be run out-of-order and trivially parallelized!
|
||||
<h3>Partial Evaluation</h3>
|
||||
Don't have the whole set of data all at once? That's fine!
|
||||
<h3>Complete Safety</h3>
|
||||
There's no such thing as a runtime error.
|
||||
</article>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -0,0 +1,64 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charaset="utf-8" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>The Switte Programming Language</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
<script type="text/javascript">
|
||||
var _paq = _paq || [];
|
||||
/* tracker methods like "setCustomDimension" should be called before "trackPageView" */
|
||||
_paq.push(["setDocumentTitle", document.domain + "/" + document.title]);
|
||||
_paq.push(["setCookieDomain", "*.lijero.co"]);
|
||||
_paq.push(["setDomains", ["*.lijero.co"]]);
|
||||
_paq.push(['trackPageView']);
|
||||
_paq.push(['enableLinkTracking']);
|
||||
(function() {
|
||||
var u="//p.lijero.co/";
|
||||
_paq.push(['setTrackerUrl', u+'foo']);
|
||||
_paq.push(['setSiteId', '1']);
|
||||
var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0];
|
||||
g.type='text/javascript'; g.async=true; g.defer=true; g.src=u+'foo.js'; s.parentNode.insertBefore(g,s);
|
||||
})();
|
||||
</script>
|
||||
</head>
|
||||
<body>
|
||||
<nav>
|
||||
<span id="navbrand"><a href="/switte/">Switte PL</a></span>
|
||||
<ul>
|
||||
<li><a href="/switte/download/">Download</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/documentation/">Documentation</a></li>
|
||||
<span> | </span>
|
||||
<li><a href="/switte/community/">Community</a></li>
|
||||
</ul>
|
||||
</nav>
|
||||
<article>
|
||||
<p>
|
||||
<strong>Switte</strong> is a programming language that uses simplicity to its advantage.
|
||||
</p>
|
||||
<pre><code>
|
||||
This is an example program.
|
||||
> ABC = mulI1 parI1 [ mulE1 ] [ lemI ] map
|
||||
</code></pre>
|
||||
<h2>Features</h2>
|
||||
<h3>Instant Relocation</h3>
|
||||
<p>Save a program mid-execution and restart it anywhere.</p>
|
||||
<h3>Flat Model</h3>
|
||||
<p>
|
||||
Arbitrary partitions of a program are equivalent.
|
||||
Programs can safely be run out-of-order and trivially parallelized!
|
||||
</p>
|
||||
<h3>Partial Evaluation</h3>
|
||||
<p>Don't have the whole set of data all at once? That's fine!</p>
|
||||
<h3>Complete Safety</h3>
|
||||
<p>There's no such thing as a runtime error.</p>
|
||||
</article>
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -0,0 +1,14 @@
|
|||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
|
||||
<head>
|
||||
<meta charaset="utf-8" />
|
||||
<meta name="robots" content="index,follow" />
|
||||
|
||||
<title>The Switte Programming Language</title>
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1" />
|
||||
|
||||
<link href="/favicon.png" rel="icon" type="image/png" />
|
||||
<link href="/res/common.css" rel="stylesheet" type="text/css" />
|
||||
|
||||
</html>
|
||||
296
switteprim.txt
296
switteprim.txt
|
|
@ -1,296 +0,0 @@
|
|||
INTRODUCTION
|
||||
=================
|
||||
|
||||
This system is derived from linear type theory, such that for a value x with type A:
|
||||
|
||||
(x : A) means that x must be used exactly once.
|
||||
(x : ?A) means that x may be used at most once, or forgotten.
|
||||
(x : !A) means that x may be used multiple times, but at least once.
|
||||
(x : ?!A) means that x may be used zero or more times.
|
||||
|
||||
? is read "why not", and ! is read "of course".
|
||||
|
||||
Additive means "there are two possibilities, but you only get one". In other words,
|
||||
in each branch of an additive relationship, all of the non-? variables in the
|
||||
context must be disposed of.
|
||||
Multiplicative means "you get both of these at once". In other words, all of the
|
||||
non-? variables must be disposed of as a whole.
|
||||
Conjunction means "both values exist at once".
|
||||
Disjunction means "only one of these values exist at once".
|
||||
|
||||
Additive conjunction (a & b) means "you can use either a or b, it's up to you which".
|
||||
Additive disjunction (a + b) means "I am going to give you an a or a b, and you must
|
||||
be prepared to deal with either, but not both at the same time."
|
||||
Multiplicative conjunction (a * b) means "I am going to give you an a and a b, and
|
||||
you have to use both".
|
||||
Multiplicative disjunction (a | b) means "you must be prepared to recieve both an a
|
||||
and a b, but ultimately only one will be used". If that's a bit confusing, that's alright.
|
||||
|
||||
|
||||
AXIOM
|
||||
=====
|
||||
|
||||
a | -a
|
||||
|
||||
where -a represents the dual of a, and | represents multiplicative disjunction.
|
||||
This is the axiom of the excluded middle, meaning to "a is true or not true".
|
||||
Its implementation is explained in "multiplicative disjunction". There are no
|
||||
further axioms.
|
||||
|
||||
|
||||
Duals:
|
||||
|
||||
While they're a general construct, the dual is actually only used for the
|
||||
definition of the axiom, so I'll specify it here:
|
||||
|
||||
-(-a) = a
|
||||
-(a & b) = -a + -b
|
||||
-(a * b) = -a | -b
|
||||
-Top = 0
|
||||
-1 = Bottom
|
||||
-(!a) = ?(-a)
|
||||
|
||||
and vice versa in all cases.
|
||||
|
||||
|
||||
Distributivity:
|
||||
|
||||
This isn't actually related to the axiom, but I might as well while I'm at it.
|
||||
None of these are built-in rules, they are just helpful notions provable within
|
||||
the language itself. These are the distributive laws:
|
||||
|
||||
a * (b + c) = (a * b) + (a * c)
|
||||
a | (b & c) = (a | b) & (a | c)
|
||||
a * 0 = 0
|
||||
a & Top = Top
|
||||
|
||||
notice how "exponentials" convert "addition" into "multiplication"-- hence the names:
|
||||
|
||||
!(a & b) = !a * !b
|
||||
?(a + b) = ?a | ?b
|
||||
!Top = 1
|
||||
?0 = Bottom
|
||||
|
||||
and vice versa in all cases in both sets listed.
|
||||
|
||||
|
||||
STRUCTURAL RULES
|
||||
================
|
||||
|
||||
The weakening and contraction rules are specified twice since
|
||||
I hope to extend this into an ordered logic, so I have to include
|
||||
the exchange-requiring equivalents. This is also true for constructors and
|
||||
eliminators in the computational rules. All of these can be implemented only
|
||||
once, with the second rule being implemented in terms of the first via a swap
|
||||
that /doesn't/ apply an unordered constraint. If I do not extend this to an
|
||||
ordered logic, you can simply ignore all of the second rules.
|
||||
|
||||
Weakening: a -> ?b -> a ### const
|
||||
?a -> b -> b ### flip const
|
||||
Contraction: (a -> !a -> b) -> (!a -> b) ### join
|
||||
(!a -> a -> b) -> (!a -> b) ### join . flip
|
||||
Exchange: (a -> b -> c) -> (b -> a -> c) ### flip
|
||||
(or equivalently (a * b) -> (b * a))
|
||||
|
||||
(todo: do I need a dual exchange rule for &?)
|
||||
|
||||
|
||||
COMPUTATIONAL RULES
|
||||
===================
|
||||
|
||||
These are the introduction and elimination rules for compound terms in the
|
||||
language. Introduction terms are labeled with an i, elimination terms with an e.
|
||||
When multiple introduction/elimination rules are required, they are each labelled
|
||||
with a number.
|
||||
|
||||
|
||||
Additive conjunction (with):
|
||||
|
||||
Topi1 : a -> a & Top
|
||||
Topi2 : a -> Top & a
|
||||
additively (all of the context is used in either branch of the options a and b),
|
||||
&i : a -> b -> a & b
|
||||
&e1 : a & b -> a
|
||||
&e2 : a & b -> b
|
||||
|
||||
The eliminators may be called "projections".
|
||||
|
||||
There is no elimination rule for Top, since it doesn't exist. It can only
|
||||
be introducted in terms of the type signatures in Top1 and Top2, and the
|
||||
only thing you can do with it is ignore it via the associated projection.
|
||||
It doesn't have to exist because nothing using the projection for Top
|
||||
can exist because it cannot be used for anything, nor weakened.
|
||||
|
||||
Additive conjunction can be interpreted as a pair of procedure pointers,
|
||||
with the context enclosed inside. The projections are function calls that
|
||||
choose which procedure to invoke to consume the context. A call to Top
|
||||
is equivalent to nontermination, since Top doesn't exist.
|
||||
|
||||
The compiler could probably safely maybe automatically insert the
|
||||
eliminators when the corresponding type is required, but I haven't totally
|
||||
thought this through, and there are potential issues with e.g.
|
||||
(a & b) & a, in the event that choice of a matters.
|
||||
|
||||
|
||||
Additive disjunction (plus):
|
||||
|
||||
0e : 0 -> a
|
||||
+i1 : a -> a + b
|
||||
+i2 : b -> a + b
|
||||
+e1 : (a -> c) & (b -> c) -> (a + b -> c)
|
||||
+e2 : (b -> c) & (a -> c) -> (a + b -> c)
|
||||
|
||||
0, like Top, does not exist. It only exists as a fragment of the type
|
||||
signature in disjunction introduction, because
|
||||
+i1 (x : A) : forall b. A + b
|
||||
and 0 is simply an instanciation of b, taking the entire forall thing
|
||||
far too literally, as shown in its eliminator. It is impossible to
|
||||
have an actual instance of 0, because by definition, it is the type
|
||||
not selected when you create a +. In terms of elimination, all eliminations
|
||||
of an 0 + a type are equivalent to (e1 0e), with the exception of the fact
|
||||
that you have to destroy anything in your context that cannot be weakened.
|
||||
This can be trivially implemented as using 0e to generate a function type
|
||||
that directly consumes all of the terms in the context, and returning a c.
|
||||
|
||||
The eliminators are rather intuitive. The choice of & is necessary because
|
||||
each option must entirely dispose of its context, as is in the definition
|
||||
of &i.
|
||||
|
||||
A value of a + b is trivial: it's just a tagged union, i.e. an indicator
|
||||
of whether it's a or b, and the value a or b.
|
||||
|
||||
|
||||
Multiplicative conjunction (times):
|
||||
|
||||
1i : 1
|
||||
1e1 : 1 * a -> a
|
||||
1e2 : a * a -> a
|
||||
*i : a -> b -> a * b
|
||||
*e1 : a * b -> (a -> b -> c) -> c
|
||||
*e2 : (a -> b -> c) -> a * b -> c
|
||||
|
||||
1 does exist, and in fact its sole introduction rule is "1 exists", but
|
||||
it holds no information, so in practice it doesn't have to be stored.
|
||||
Formally it has only one elimination rule, 1 -> <nothing>, but a function
|
||||
can't return nothing, so instead you have to eliminate it via its definition
|
||||
as the identity element.
|
||||
|
||||
The rest of it is pretty intuitive. In memory, it's just a pair of values.
|
||||
|
||||
|
||||
Multiplicative disjunction (par):
|
||||
|
||||
Bottomi1 : a -> a | Bottom
|
||||
Bottomi2 : a -> Bottom | a
|
||||
Bottome : Bottom -> a
|
||||
|i : ?a * ?b -> a | b
|
||||
|e1 : ?(a -> c) * ?(b -> c) -> a | b -> c
|
||||
|e2 : a | b -> ?(a -> c) * ?(b -> c) -> c
|
||||
|
||||
Multiplicative disjunction is by far the least intuitive operator, corresponding
|
||||
to delimited continuations and functions.
|
||||
|
||||
Bottom does not exist. Like with additive disjunction, it's just part of
|
||||
the type signature, and it simply exists to not get chosen.
|
||||
|
||||
As you can see, |e produces only one c despite having two options, both
|
||||
of which are provided in |i. That's because |e is inherently
|
||||
nondeterministic. |i and |e are both entirely weakened because neither
|
||||
choice will necessarily be chosen, yet they both must exist in full. This means
|
||||
the entire closure that they are in must be somehow weakened, since it's
|
||||
not possible to dispose of a full value in both branches at once, because
|
||||
that would constitute double use. The use of the * in the signature is to
|
||||
emphasize the relationship to multiplicative conjunction and that behavior,
|
||||
just as additive disjunction is defined in terms of additive conjunction.
|
||||
|
||||
A par value is implemented in terms of a pair of function calls. In the
|
||||
eliminator, either function may be invoked, and when the value is used,
|
||||
the eliminator may choose to forget the function halfway through and jump
|
||||
to the other option instead, making it equivalent to a continuation, the
|
||||
functional equivalent to a goto.
|
||||
|
||||
The main use of par is in the sole axiom of the excluded middle, which encodes
|
||||
the equivalent to functions and delimited continuations. For reference, the type
|
||||
of a function is defined as (a -> b = -a | b). Essentially, the axiom can't pull
|
||||
a value of type A out of thin air, so it is forced to choose the -a branch.
|
||||
-a is equivalent to a -> Bottom, and therefore can only be used by providing a
|
||||
value of type a, so instead of actually providing that Bottom, the function
|
||||
simply jumps to the branch that demanded an a in the first place and returns
|
||||
that result. Functions are implemented the same way, only kinda in reverse:
|
||||
it runs the side that claims to have an extra a it needs to dispose of, and then
|
||||
once it gets that hole, it produces the a in the other branch and terminates.
|
||||
Implicitly in either case the context is consumed, which is equivalent to the
|
||||
function returning. As you can see though, these are simply different
|
||||
perspectives on the same axiom.
|
||||
|
||||
If you don't get it, that's fine, because it's super confusing, and I don't
|
||||
understand it either.
|
||||
|
||||
|
||||
TYPECLASSES & MODULES
|
||||
=====================
|
||||
|
||||
I haven't really figured out typeclasses. Basically I intend for them to be
|
||||
existential types (via dependent sums maybe?), but I need to figure out how to
|
||||
make it practical first.
|
||||
|
||||
Requirements:
|
||||
* It must be possible to use the instanced values without having to unwrap the
|
||||
class implementation manually first.
|
||||
* It must be possible to use the function instances equally easily, and without
|
||||
having to declare the names at each usage point.
|
||||
* They must permit non-unique instances.
|
||||
* Instances must be stackable, the outermost one being used unless the inner one
|
||||
is exposed within one of the instance type-contextual manipulations (e.g. functor).
|
||||
This is important especially since Copy should implement !, but it should be
|
||||
possible to rc a copiable variable and have it behave as expected. Copy is
|
||||
described in more detail in Mutation.
|
||||
|
||||
Modules are essentially the same thing as typeclasses, and have similar
|
||||
requirements. The answer to both probably lies in the same place. Lightweight
|
||||
modules that are as easy to use as typeclasses would be a major plus too.
|
||||
|
||||
I don't suspect this problem will be all that hard to resolve.
|
||||
|
||||
|
||||
As far as ! and ? go, they are essentially typeclasses. @ below is a typeclass
|
||||
too. Essentially, these are the introduction rules for ! and ?, though these
|
||||
are not possible to derive without external functions (for obvious reasons),
|
||||
and being typeclasses, it's not appropriate to give them introduction rules.
|
||||
|
||||
To specify a !, you need a class instance satisfying either the contraction rule,
|
||||
or equivalently, the following:
|
||||
!i : a -> !(() -> a)
|
||||
|
||||
To specify a ?, you need a class instance satisfying either the weakening rule,
|
||||
or equivalently, the following:
|
||||
?i : a -> ?(a -> ())
|
||||
|
||||
The reason these are essentially introduction rules is made more obvious if you
|
||||
wrap the entire thing into a (-> !a) or (-> ?a) respectively.
|
||||
|
||||
|
||||
MUTATION
|
||||
========
|
||||
|
||||
@ means "mutable" to the compiler. Normal values are immutable, which means to
|
||||
make changes, the entire object has to be deconstructed and reconstructed again.
|
||||
Mutation allows direct modification to the data structure without concern.
|
||||
Generally things are mutable by default, but this may not be the case with
|
||||
external values, or internal values via pointers.
|
||||
|
||||
@ extends ?, which means a mutable pointer may be freed, but not !, so that
|
||||
you cannot have multiple instances of a mutable pointer.
|
||||
|
||||
Losing mutation in favor of replication:
|
||||
rc : @a -> !?a, introducing a reference-counted pointer
|
||||
|
||||
Some values may implement Copy, allowing deep duplication. All composite
|
||||
structures may automatically derive Copy whenever both of their constituents
|
||||
are !. Copy, of course, is an implementation of !, though using (rc) anyway
|
||||
may be desirable for performance reasons, especially for highly composite
|
||||
structures.
|
||||
copy : Copy a => a -> @a
|
||||
|
||||
Generally, syntactic sugar should eliminate most of this crap such that the
|
||||
programmer shouldn't have to deal with it most of the time.
|
||||
|
|
@ -0,0 +1,27 @@
|
|||
* Highly parallel processing-- distribute code over CPU cores, GPU cores, or computers on a network-- completely transparently.
|
||||
* Free networked programs-- location-agnostic code can be run anywhere or everywhere, and multi-user systems via a multi-entry point program.
|
||||
* Streamable computations-- computation can begin even when not all of the data has arrived yet.
|
||||
* High performance-- simple and fast computations on CPU or GPU, easy to compile.
|
||||
* Hard real-time, strict determinism-- extremely simple program semantics and implementation allow making very strong guarantees, including precise computation times and results.
|
||||
* Secure-- deterministic and provable program behavior allows trivially creating secure subsets of the language.
|
||||
* High-quality debugging tools-- the compiler is aware of a large amount of metadata for generating messages, and program images allow easy reproducibility/analysis.
|
||||
* Portability-- no programming language behavior is platform-dependent, so only calls to native libraries are platform-dependent.
|
||||
* Provable correctness-- everything else not good enough for you? prove your programs correct using the formal semantics.
|
||||
* Low- or high-level-- the programming language depends on virtually no runtime (just malloc), not even a garbage collector, and would be suitable for writing OS-level code wherever C would be. In fact, it could be feasible to implement Switte as a CPU instruction set.
|
||||
* High-quality type inference-- strongly and statically typed, but you'd never know it.
|
||||
* Code inference-- built-in proof helper can automatically infer your code based on its type.
|
||||
* Highly granular versioning-- hash and graph-based version control applies not just to libraries, but individual functions and types. This could theoretically be used for a completely decentralized/distributed package manager.
|
||||
* High-quality documentation-- every aspect is formally specified and explained for academics, developers, or laymen, such that anyone can learn it.
|
||||
* Extreme simplicity-- a very small yet complete set of primitives and virtually no syntax makes learning or porting it easy.
|
||||
* Extensibility-- if you don't appreciate the simplicity, you can simply encode your favorite syntax or language structures directly into the language.
|
||||
* Mathematician- and logician-suitable-- basis in a very general type theory makes it suitable for mathematicians (though unfortunately it is not Homotopy-based)
|
||||
* Linguist-suitable-- the Lambek fragment is suitable for describing categorical grammars
|
||||
* Staticstics interpretation-- the non-associative fragment corresponds with concepts in statistics.
|
||||
* Programmer-suitable-- if you don't care about all that stuff, the full fragment is Turing-complete and a suitable programming language.
|
||||
* Native literate programming support
|
||||
* Rich code editing-- textual source code is possible but unneccessary. Compiled code and source code are essentially equivalent, so between the instruction set and hash-graph VCS, it is possible to interact with code entirely non-textually.
|
||||
* Eager or lazy?-- irrelevant! Switte's linear semantics make evaluation strategy definitionally irrelevant. In other words, Switte is strongly normalizing (with a few exceptions related to the full fragment).
|
||||
* Stateless-- dump a running program and restart it anywhere. You might even argue that all Switte programs are always running, in a sense.
|
||||
* Flatness-- Switte has no syntax, and therefore arbitrary partitions of programs are equivalent.
|
||||
* Simplicity-- a very small set of primitives and no syntax.
|
||||
* Derived from type theory-- clear formal semantics makes it easy for both humans and compilers to reason about programs.
|
||||
Loading…
Reference in New Issue