Challenges & Expectations – Interview with e-Orzecznik.pl

[Audio bells]

Welcome Marek, Welcome., Would you provide some insight into how E-Orzecznik came to be, and what drove the creation of this ambitious project?

Marek:  Definitely, Peter. 

The idea behind E-Orzecznik was inspired by the real-life experience of our co-founder, Christian.  He started and ran an Occupational Health Clinic. He assessed the different software options that were available then in the market  and was engulfed by difficulties in digitizing and managing patient records. 

This experience led Christian to develop the idea for E-Orzecznik.  It was back in 2017, and there was no multi-user software solution available. So we recognized the potential in this gap and funded the venture ourselves.

Peter: So then most software companies back then didn’t cater to occupational medicine in Poland.  How did the game change when E-Orzecznik joined the scene?

Marek: Occupational Medicine in Poland is a small branch of the healthcare system with relatively complex administration requirements.  Providers of software for conventional medical documentation have often overlooked the specific needs of Occupational Physicians.  As a result, the solutions they offer lack the sophistication needed to manage the extensive documentation requirements of occupational medicine. 

We took a different approach to this underserved market in 2021, with the launch of our software.

Peter: Developing this software was clearly not an easy or short journey. Let’s talk about some major milestones on your path from the initial idea up to platform launch.

Marek: The development process was indeed challenging, largely due to the complexity and extensive paperwork requirements of occupational medicine that discouraged the mainstream software providers. To serve occupational physicians effectively, we had to bring together dozens of complex procedures, each involving lots of documents and hundreds of forms to be filled, with complex validation rules.   We quickly realized our success depended on managing and swiftly updating these dependencies. 

We rose to the challenge and officially launched the software in February 2021.

Peter: How did it go? and how did the pandemic affect the launch?

Marek:  The timing of the launch was certainly unique. Firstly, it happened as you said during a pandemic that caused a lot of sudden changes around occupational medicine.  Additionally, new rules demanding further digitization were being implemented by law. 

Our early customers welcomed our interface as very user-friendly and they played a critical role in improving the software. Their feedback and ideas have been crucial in shaping our journey and our commitment to customer engagement.

Peter: As E-Orzecznik has grown, can you share some key metrics or anecdotes that reflect your progress since it was first conceived?

Marek:  We’ve seen consistent growth every month since our launch, and an insignificant  churn rate. Our customer reviews show we have achieved a very high rating, and this is  from professionals who use our tool daily.  Implementing innovative technologies has set us apart from our competition. 

Most of our competitors built traditional desktop applications.  We also offered a clear  web application pricing model.  Thanks to our user interface and intuitive user experience, most of our users started interacting with our software without any dedicated training. This is quite common in modern software applications, but it was a new development in the field of medical software. This is why we’re really excited about our upcoming work with Formal Foundry.

Peter: Thanks for that Marek. We are excited for that as well and appreciate the opportunity.

I understand there are some unique challenges you encountered while developing your software that actually make this relationship really useful for both of us.

Marek:  The landscape of occupational medicine is complex, with many procedures and knotty validation rules.  Managing all the requirements, and still having a user friendly and simple interface was a main challenge.  To manage the complexity we introduced a Domain Specific Language (DSL) and a WYSIWYG (What You See Is What You Get) tool for developers.  This additional layer of abstraction has proven quite beneficial.  It also makes the use of FormalFoundry’s tool a great fit.

Peter: This is something innovative on the part of E-Orzecznik. How was the initial reception in the market? And what challenges related to the industry have you faced the most?

Marek: At first, there was some distrust. We were one of a very small number of companies selling Software as a Service (SaaS) within this domain.  It’s also most interesting because our architecture provided superior data security.  Data security is a feature that is often ignored by individual users mostly due to a lack of dedicated IT support at their companies.  So having this feature embedded, really sets us apart from the other industry players.

Peter: Dealing with healthcare data, especially occupational medicine that not only involves medical data but also employment data, comes with regulatory and legislative complications for most places in the world, at this point.  Would you elaborate on how you navigated the sophisticated regulatory landscape in Poland?

Marek:  Navigating the regulatory and legislative environment was indeed a crucial challenge. Much of the Polish legislation was not considering electronic medical documentation for occupational medicine.  So the challenge was not in meeting high standards, but in defining exactly what the high standards should really be.  

Peter:  Well that’s a great place to be if you are starting something.

Marek:  Well, we had to go from scratch.  Many of the rules are inconsistent.  So we asked legal professionals for their opinions, and then we initiated dialogues with government authorities, so we could interpret the rules correctly in our platform. We also needed to provide unique and legally binding biometric signatures for patients in order to comply. 

To minimize friction, we decided to develop our own internal solution based on European Union standards.  This also gives us some strategic advantages, so it’s worth it.

Peter:  So, Marek, as you well know, FormalFoundry’s tools are all about provable correctness.   Our listeners might like it if you delve further into how critically important this concept of correctness already has been for E-Orzecznik, in delivering high-quality software and safe digitizing of medical records.

Marek: Absolutely, Peter. 

At E-Orzecznik, we believe that ensuring accuracy in our software from the very start of our development process is fundamental to delivering superior products.  Unfortunately, this viewpoint is not widely acknowledged in the software industry. As the software sector has rapidly evolved over the last few decades there still persists the notion that if your software passes testing, then it must be correct. 

However, with growing software complexity it becomes increasingly apparent that tests cannot cover every possibility.  The potential complexity of software states is amazingly vast, and aspects such as the use of the UI in the field by medical staff are simply difficult to test comprehensively.

To address these ‘blind spots’, we believe that we must deeply consider the correctness of our software right from the beginning,  which takes time and effort and some difficult work for developers.  This philosophy is reflected in the way we applied a Domain Specific Language (DSL) to our architecture.   Although this new layer of abstraction ironically increases the complexity of the software,  it actually creates a structure that naturally isolates bugs across our system layers.  This makes it possible to handle them and more levels of complexity.

Peter: That’s a very progressive approach. What about the impact of errors or inaccuracies on the whole client ecosystem?

Marek:  That’s an excellent question. 

Our software is not a mere value-add for our clients – it’s their primary tool, which is crucial to their business, for them to do their job.   There is no tolerance for errors or downtime.  Any and every error is a disaster and a disruption. So we simply don’t want any errors despite all this complexity. 

And because of the high stakes involved, data breaches or inconsistencies are absolutely unacceptable in our field.  So the more we can do to eliminate errors and breaches, the better our software will be, and we have proven that using the DSL we developed.

Peter: So then “correctness” seems to be, really is a significant part of your value proposition already. Would you discuss the impact it has on your customers’ trust and experience?

Marek:  Safety and accuracy have been a key part of our strategy from the beginning.  A foolproof UI is part of that as well.  The usability focus can also slow us down on our development pace.  But these are sacrifices we’re willing to make to help guarantee correctness. 

But like I said, correctness is hard.  Given the detail oriented and complex workflows we encounter regularly in our industry, we are sometimes pushed to a trial-and-error approach to find the right solutions.  This can be very time consuming if you want to be as accurate and correct as we want to always be. So this is why we are betting that automated formal verification systems together with large language models, will be the key to accelerating our market growth. 

We expect FormalFoundry is going to help make our workflow implementations even more correct  and that this will make us an even clearer best choice solution in our industry.

Peter: Well you know I am excited for that as well, Marek.  So, I have learned that you already, in a short time after starting in 2021, that you have captured a healthy piece of the market from other entrenched players.  But what is your strategy and philosophy going forward into such a tight competitive space?

Marek:  Well, we are a small company serving a limited market.  We don’t have the luxury to strategize for lengthy periods as we can expect competitors to try to beat us back as best they can. 

We think we can be further recognized and become even more competitive if over time our market sees we are error free, secure, and easiest to use.  So if we can automate formal verification of our software, so that it is practical, so that trial and error are eliminated, then we will win more business in our market. 

When we made the strategic decision to integrate automated formal verification into our software, we made sure that our entire team of developers agreed with the decision. After our past success with the DSL, it’s now a part of our team’s technical culture to innovative and try new and better programming techniques all the time.

Peter: So what options did E-Orzecznik consider to enhance system security and efficiency using FormalFoundry’s approach to verification?

Marek: After deciding to collaborate with FormalFoundry, we identified areas where such an approach would be most beneficial. 

We consider measures of application security to ensure no data breaches could occur, and the accuracy of our access control system.

Peter: What about strategies to mitigate runtime errors?

Marek: We considered that as well, Peter. 

We thought about proving the absence of runtime errors and the reliability of load balancing. Given certain environmental and traffic assumptions, we were confident that our systems would remain responsive and that backups would always function promptly.  There are some risks but complexity level is lower.

Peter: Data integrity is, I assume, very critical in your field. What strategies did you consider to ensure this aspect of your software?

Marek: You’re right Peter. 

We took a serious look at verifying the reliability of our abstract workflows and data schemes for forms, which are part of these workflows. This is relatively unusual in generic software.

Peter: After reviewing these options, what eventually emerged as your ‘killer app’?

Marek: We see the potential of our DSL for workflows. It was perfectly suited for formal verification with its abstraction. 

The business impact also played a huge role. Organic development and quality assurance life cycles had caused this aspect of our system to be time-consuming and challenging. To ensure correctness manually for complex dependencies is barely possible and very time-consuming.

Peter: Would you elaborate on that?

Marek: Sure. 

Serving runtime errors and system stability are more typical targets for formal verification but for us they seemed comparatively generic. To hold a medical procedure or documentation with ensured accuracy is very specific to our industry and promises to be our biggest advantage. 

It’s also clearly good for economic reasons – much more time is spent trying to ensure the accuracy of these specific workflows than on the more generic parts of our system. So, we believe that this is  the right move, that promises us a competitive edge and a big positive impact on our business and growth.

Peter: I see.  So, Marek, could you share with us the implementation plan you established after deciding on the focus areas, and also what you initially expected from the Formal Foundry team?

Marek: Sure!  

At the beginning I was afraid that the Formal Foundry team would choose a lean approach, without specific goals, and act through a trial-and-error method. I wrongly assumed the uncertainty over what might prove effective considering the novelty of the technology. 

What happened next was  the exact opposite. The team selected a method that was quite precise, aiming to restrain uncertainty and provided possible-to-measure results. 

That was impressive and exceeded my expectations.

Peter: That’s insightful, Marek. What is the next step in the process after you and the Formal Foundry team have made these initial agreements?

Marek: Well, now we are focused on updating and creating new forms with intrinsic logic schemes.  These forms consist of hundreds of different fields and are built in our specially designed WYSIWYG editor for our DSL.  We ensure proper logic by writing snippets of code in a subset of JavaScript, which delivers proper user interaction with the form. Even though these pieces of code spread throughout the forms used only for specific data field validation. 

This way the risk of a bug has been limited to a small area. But the large number of fields and multiple contexts of their value add an incredible layer of complexity. It’s very challenging to test.

So we thought we would support this process with a conversational assistant that uses a large language model. But trying to use LLM’s naively could result in a lot of inconsistencies and finally would be counterproductive.  And this is precisely where Formal Foundry’s technology comes into play, and, we expect, will make a big difference. The assistant with a large language model provides the main tool which  proves the validity of the responses. 

Imagine, if a developer asks questions about the code in natural language — for example, if they want to verify if the workflow always ensures some additional exams before granting work permission. The developer can trust that given an affirmative response from the assistant it’s not due to a software hallucination. Every response from the system will be backed by a proof assistant, ensuring that an answer is only given if the LLM outcome is accepted by the proof assistant. This is consistent and impossible to deceive.  This makes the assistant protected from hallucinations.

Q22

Peter: It sounds not just fascinating but also quite futuristic, doesn’t it?

Marek: Without a doubt this seems like some distant future.  It’s hard to believe that result correctness can be proven for big complex programs. But we think the  Formal Foundry tool will make it a reality within the next six months.

Peter: Could you talk some more about the initial stages of developing this exciting tool?

Marek: In the next step the formalization of certain domains  will be built with Agda, a widely used proof assistant.  Meaning, a proof assistant that is frequently used to substantiate things about formal systems needs to formalize our domain into the very expressive but specific language it uses.  After this, we’ll try to express some aspects of our workflows in Agda to test the effectiveness of the proving system.

Peter: Sounds like a rigorous process. Do you foresee any unique challenges arising at this stage?

Marek:  It’s hard to predict what will be straightforward and what could present challenges. But considering the initial promising experiments and performance already demonstrated, we think there will be considerable overlap between what is practicable and what will be really useful for us.

Peter: Should the testing phase proceed smoothly, what would be the next milestone in your collaboration?

Marek:  With the results of these experiments in hand, we plan to proceed to implement the FormalFoundry tool for our developers.  We aim to integrate the resulting layer seamlessly into existing tools for developing workflows. 

Really our current tools and existing domain-specific language abstractions align well with the idea of formal reasoning.  We already have some custom development tools that provide us with the right environment to experiment with this type of technology.  So we are expecting a great outcome.

Peter: I’m expecting that too!  Marek, could you talk to us a bit about the potential impacts this partnership between E-Orzecznik and Formal Foundry might have on the company? Specifically, I’m interested in any improvements in system efficiency or error reduction that you anticipate.

Marek: Of course, Peter. 

From the degree of automation demonstrated by the Formal Foundry demos we’ve seen so far, we expect a significant improvement in productivity among our domain developers.  A significant portion of the work we are striving to automate is not necessarily difficult from a logical perspective, but it’s more mundane and repetitive. Such tasks cannot be automated without a reasoning system boasting a certain level of flexibility and expressiveness and narrowly focused on the domain.

Peter: Fascinating. What do you think the effect will be on your company’s engineering culture?

Marek: We believe that bold investments in cutting-edge technologies, even those not yet widely applied in the software industry, locks into our culture. We think it’s essential not just to keep up with existing industry standards, but also to be the ones setting the pace. That’s our engineering and business culture.

Peter: Ok. Then adopting a safety tool like ours aligns well with your culture.

Marek: Exactly.  We believe the software industry is still in its early stages with myriad techniques narrowly applied. Now with AI to assist us, we think the shift is transformative.  Finding a way to assure and prove correctness as we shift up the AI road will completely alter the paradigm of safety-critical software and the general use of LLMs. 

This is why we are working with you guys. But also, it’s economical for us to do this with you.  At the end of the day, when your tools are built, we expect our customers will receive the benefit through faster, super accurate software for healthcare forms and workflows. 

Also, we see that the solution may also bring increasing customizability to the table for our clients. At present, only our biggest customers can afford such services.  In fact, we think the FormalFoundry tech could be key to transforming our market position and giving us a heightened strategic advantage.  The safe and accurate use of AI will absolutely bring us down the cost curve.

Peter: Well that certainly paints a picture of a promising future, Marek. 

Thank you so much for your insights today. I sincerely believe our listeners will appreciate the revolutionary perspectives you’ve shared here.

Marek:  Thank you for the opportunity to speak to your audience,  and it was a pleasure spending some time together. 

Let’s talk again soon.

[insert selfies]