If you go to their cloud service page (https://cloud.internalpositioning.com/), it's trivially easy to get live location data for strangers by guessing names.
Yikes, you are right. Just typed in "Jones" and it loaded up a dashboard with a bunch of data. Fortunately it appears to be someone playing around with the dashboard. If you zoom out on the map, all the GPS markers make a smiley face :)
Their only distribution center, at that! They ship everything out of the Thief River Falls warehouse. They also run a great tour, if you're ever in the area.
Fun fact, they can take just about any combination of the 1million+ SKUs they stock from order reception to in a box waiting for a truck in under 15 minutes.
They have (had?) a local warehouse I think off 101 in the Bay Area, don't remember exactly where. You could walk in with a list of parts and they would grab them for you right there.
Yep thanks I just remembered that's what it was ("it had a J in it"). Woops. Not sure why I've had them confused for Digi-Key the last few years. Maybe the Digi-Key branding is just more memorable.
"The Muen Separation Kernel is the world’s first Open Source microkernel that has been formally proven to contain no runtime errors at the source code level."
This doesn't really jibe with seL4's claim: "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is now open source." http://sel4.com/
The issue here is the spec - no runtime errors at the source code level is, as I understand, a completely different specification than end-to-end implementation correctness.
In particular, the Muen Kernel report itself [1] explains:
By implementing the kernel in SPARK and proving the absence of runtime errors, we have
shown that the kernel is free from exceptions. While these proofs provide some evidence to
the correctness claim of the implementation, the application of these particular formal methods
do not provide any assurances beyond the error free execution of the kernel. Proving functional
properties such as the correspondence of the scheduler to a given formal specification is necessary
to further raise the confidence in systems based on the Muen kernel.
In other-words, we don't yet have formal confirmation that this thing actually does what we might expect it to - just that its execution is bug-free.
But in the other direction, it seems that end-to-end implementation correctness implies absence of run-time errors. The seL4 authors write[1]:
> IMPLICATIONS [...]
a functional correctness proof already has interesting implications for security. If the assumptions listed in Sect. 5.5 are true, then in seL4 there will be:
No code injection attacks [...] No buffer overflows [...] No NULL pointer access [...] No ill-typed pointer access [...] No memory leaks [...] No non-termination [...] No arithmetic or other exceptions [...] No un-checked user arguments [...] Aligned objects [...] Wellformed data structures [...]
And this was already done in 2009. So I don't think Muen is the first microkernel to prove absence of run-time errors. (Maybe they claim that Muen is the first open source run-time-error-free microkernel in the sense that they did the verification after seL4, but before seL4 was open-sourced?)
I would guess so, seL4 was open sourced in August 2014 and the first public preview of Muen was December 2013, per a quick check with Google.
On the other hand, I've read that if you want to do serious SPARK/Ada work, you've got to buy AdaCore's tools or benefit from their academic program. seL4's verification down to binary was done using generic GCC (a clever way was found to meet the higher level proofs with stuff generated from the binary; they first tried CompCert (a verified C compiler that is free for non-commercial use) but I gather that suffered from an impedance mismatch).
Lots of free guides, tips, libraries, etc. You get way better tools in terms of testing, inspection, analysis, etc if you buy them. No doubt. The base platform, good enough for Muen or IRONSIDES DNS, is free. You can replicate their work easily plus create safer variants of established software such as Nginx, etc.
Whereas seL4 relies on Haskell, Isabelle, several proof frameworks/tools, C, and GCC. They achieved a lot more but with a lot more tools, time, and expertise. Those of us that were interested couldn't even check the verification stuff, especially the C-related tech, until late 2014. Using them would be... non-trivial to say the least. :)
Good that they open-sourced as that will allow (is allowing) others to build on the work. I know it's already getting integrated into Genode OS.
As I was told in a HN discussion that non-educational "for GPL" version doesn't supply the same runtime, and the run time supplied is not very good. Maybe it's OK, but with all those restrictions and limitations it just didn't sound like an ecosystem I want to mess with. Plus I prefer to be able to develop and release software with less restrictive open source licenses.
WRT seL4 vs. Muen, I wouldn't be surprised if seL4 does less for you, it's only 9,000 lines of C code, and some of it is artifacts from the manual Haskell -> C translation.
Ahhhhhh. Wasn't aware of that. Will have to check with them. Muen uses the zero-runtime profile. Not sure about IRONSIDES. Far as those using a runtime, if that's the case, I'd recommend some FOSS people create an alternative one that is good. Then they get the language, toolset, etc benefits without that issue. Recreating those will be much more difficult.
"WRT seL4 vs. Muen, I wouldn't be surprised if seL4 does less for you, it's only 9,000 lines of C code, and some of it is artifacts from the manual Haskell -> C translation."
That's not what I meant. seL4 is a separation kernel: they're supposed to do almost nothing. The thing is that once a modification occurs, it can invalidate the whole security claim. So, the person modifying it needs to be able to correctly use whatever its assurance depended on. That will be much easier for Muen given a domain expert only needs to learn Ada/SPARK vs all that went into seL4.
Now, Muen certainly has less assurance in that it doesn't have formal models of design, security policy, etc. Most FOSS types won't do all that, though. So, just requiring a language that knocks out errors and maybe learning Design-by-Contract is a nice alternative that might get more people involved. That it's Ada... might get less people involved. Who knows. (shrugs)
Exactly. It is exactly equivalent to saying that if a strict FP program compiles it is "bug free" but of course it has little to say about whether the code is 'correct'.
There is no Machine. There never was any Machine. The Machine is an urban myth, a grand illusion, something to give your life meaning, but which is in fact not there.
Someone probably made a nice sum from the temporary stock bump...
I have a friend in HP who actually had a job on The Machine until the "hiatus." She got switched to another project when it got put on hold... but HP was actually assigning human resources to it at one point, not just making press releases.
My read on The Machine was that HP was developing the system in parallel with the memory component.
The idea was "imagine if you had a server with an insanely huge amount of non-volatile SRAM (that could hold OS, applications, and files), and no hard disk"
It was the "huge amount of non-volatile SRAM" part that the memristor was supposed to deliver and didn't.
I thought they just pushed that part of the project back. Didn't they announce that "the Machine" is still coming, just that first iterations will have a more traditional architecture?
A friend emailed them for small quantity pricing a while ago.
"Thank you for contacting us. Our 16 pin package is the newest offering in our Neuro-Bit line of memristor products. Single packages are $240.00 USD each. We are offering a 5% academic discount on all of your purchases. The 16 pin dip will be available for shipping late-May and we are taking pre-orders now."
Eh, depends on where you're coming from. These clearly aren't "production grade." Maybe not even "academically curious grade." Until you can at least get budgetary pricing without sending someone an email, it probably isn't even worth investigating unless you're just intensely curious.
Never mind that $240 for 8 fragile, difficult-to-work-with memristors is definitely not cheap.
While I agree that they're not production grade, $240 is well within the budget of, say, a EE research lab that wants to experiment with memristor-based circuit topologies and has the equipment+expertise to handle them properly.
Points well taken, but if they're the only people selling anything like these, they can set whatever price they like. Higher prices also restrict their support efforts to serious people who know how things work.
Processing power is only one part of the equation, though. These Cortex processors are significantly more constrained in RAM and storage than computers of 1995. Run Python on a 100MHz Pentium with 192 KiB of RAM, I'll be impressed.
That's golden news! ("news" in a sense "new is well forgotten old"). I heard about bunch of previous small Python implementations, but never about that one. As a MicroPython contributor, I'd be proud to think of it as MicroPython's spiritual ancestor. It is even an 1.5.2 port, wouldn't think someone attempted to space-optimize CPython (MicroPython is developed from scratch, CPython3 hardly could be shrunk into that).
For you reference, MicroPython can start up in as little as 2K of heap. Of course, one hardly can execute something more than a simple expression like "1+1" in that memory, but 2K also include memory required for interactive interpreter (and parsing into AST and compiling into bytecode).
The company I work for, Techshot (http://techshot.com/), is currently looking to fill a couple of positions. We're a small contract engineering firm located just outside Louisville, in Greenville, Indiana. We focus on high-tech development, with most of our contracts coming from the government. We do a ton of work for NASA, DoD, NHS, and others, in addition to corporate and start-up clients.
We've been in business for 25 years, sent multiple payloads up on the Space Shuttle, built several new medical devices, and spun off a business making rugged LED lighting. We recently sent a payload up to the ISS, and we're under contract to deliver several more! With only 36 employees, it's a great work environment, with lots of schedule flexibility, and freedom to "go your own direction" with projects. We're currently looking to fill two positions: A Software Engineer and a Machinist.
Looking for a general purpose machinist who can turn parts around rapidly when necessary. We shop out a lot of stuff, but sometimes we need to make things quick. If you have less experience than requested, but can demonstrate the ability to learn quickly, it's still worth applying.
Any software engineer would need to be reasonably comfortable with low-level interfacing with hardware. Embedded development experience a huge plus. Our software interacts with lower-level embedded device we've developed in-house, giving users a nice front-end interface, and offloading some of the heavy computational lifting.
I'm an Electrical Engineer here, and I can pretty confidently say that it's a great job for a technically curious engineer. There isn't a lot of opportunity to move "up the management chain" within the company, but the work environment is super-flexible, the projects are technically interesting and challenging, and the current team is intelligent and motivated.
If you have any questions about the company, job postings, or would like to submit your resume/cover letter, send me an email, bluyster@techshot.com.
That works once you've reached a certain level of understanding. Most AAA games have really good translations.
The trick is "comprehensible input." If you can provide a learner with input that is just a little beyond their level of comprehension, they will learn much, much faster. Dump someone into an ocean of complex grammar and vocabulary? It's a nightmare. I can see definite value in a game that starts very basic, and increases complexity as you acquire a language.
A game would also be good for reinforcing word-image links without translation. Sites like DuoLingo do a very good job at training people to be translators, but a poorer job of training people to become adequate speakers, writers, and listeners.
